Nuprl Lemma : sub-bag-equal

[T:Type]. ∀[b1,b2:bag(T)].  (b1 b2 ∈ bag(T)) supposing (sub-bag(T;b1;b2) and sub-bag(T;b2;b1))


Definitions occuring in Statement :  sub-bag: sub-bag(T;as;bs) bag: bag(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  sub-bag: sub-bag(T;as;bs) exists: x:A. B[x] member: t ∈ T prop: uall: [x:A]. B[x] top: Top subtype_rel: A ⊆B all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a squash: T true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  equal_wf bag_wf bag-append_wf bag-append-assoc bag-append-empty bag-subtype-list bag-append-cancel empty-bag_wf bag-append-eq-empty squash_wf true_wf iff_weakening_equal sub-bag_wf
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin cut hypothesis equalitySymmetry hyp_replacement applyLambdaEquality introduction extract_by_obid isectElimination cumulativity hypothesisEquality equalityTransitivity sqequalRule isect_memberEquality voidElimination voidEquality applyEquality dependent_functionElimination independent_isectElimination lambdaEquality imageElimination because_Cache natural_numberEquality imageMemberEquality baseClosed universeEquality independent_functionElimination isect_memberFormation axiomEquality

\mforall{}[T:Type].  \mforall{}[b1,b2:bag(T)].    (b1  =  b2)  supposing  (sub-bag(T;b1;b2)  and  sub-bag(T;b2;b1))

Date html generated: 2017_10_01-AM-08_53_08
Last ObjectModification: 2017_07_26-PM-04_34_40

Theory : bags

Home Index