### Nuprl Lemma : sub-bag-empty

`∀[T:Type]. ∀[b:bag(T)].  uiff(sub-bag(T;b;{});b = {} ∈ bag(T))`

Proof

Definitions occuring in Statement :  sub-bag: `sub-bag(T;as;bs)` empty-bag: `{}` 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]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q`
Lemmas referenced :  sub-bag_wf empty-bag_wf equal-wf-T-base bag_wf sub-bag-equal empty-sub-bag sub-bag_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality axiomEquality rename baseClosed universeEquality independent_isectElimination dependent_functionElimination hyp_replacement equalitySymmetry Error :applyLambdaEquality,  equalityTransitivity sqequalRule independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    uiff(sub-bag(T;b;\{\});b  =  \{\})

Date html generated: 2016_10_25-AM-10_26_46
Last ObjectModification: 2016_07_12-AM-06_42_53

Theory : bags

Home Index