### Nuprl Lemma : bag-member_wf

`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)].  (x ↓∈ bs ∈ ℙ)`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag: `bag(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-member: `x ↓∈ bs` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` so_apply: `x[s]`
Lemmas referenced :  squash_wf exists_wf list_wf equal_wf bag_wf list-subtype-bag l_member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality productEquality applyEquality because_Cache independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    (x  \mdownarrow{}\mmember{}  bs  \mmember{}  \mBbbP{})

Date html generated: 2018_05_21-PM-06_24_48
Last ObjectModification: 2018_03_23-PM-01_22_22

Theory : bags

Home Index