Nuprl Lemma : single-bags-equal

`∀[T:Type]. ∀[x,y:T].  uiff({x} = {y} ∈ bag(T);x = y ∈ T)`

Proof

Definitions occuring in Statement :  single-bag: `{x}` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` all: `∀x:A. B[x]`
Lemmas referenced :  bag-member-single bag-member_wf equal_wf bag_wf single-bag_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality productElimination independent_isectElimination equalitySymmetry hypothesis hyp_replacement Error :applyLambdaEquality,  cumulativity sqequalRule dependent_functionElimination dependent_set_memberEquality applyEquality lambdaEquality setElimination rename setEquality independent_pairEquality isect_memberEquality axiomEquality equalityTransitivity

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].    uiff(\{x\}  =  \{y\};x  =  y)

Date html generated: 2016_10_25-AM-10_27_20
Last ObjectModification: 2016_07_12-AM-06_43_29

Theory : bags

Home Index