Nuprl Lemma : bag-mapfilter-empty

P,f:Top.  (bag-mapfilter(f;P;{}) {})


Proof




Definitions occuring in Statement :  bag-mapfilter: bag-mapfilter(f;P;bs) empty-bag: {} top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] empty-bag: {} bag-mapfilter: bag-mapfilter(f;P;bs) bag-filter: [x∈b|p[x]] bag-map: bag-map(f;bs) member: t ∈ T top: Top
Lemmas referenced :  filter_nil_lemma map_nil_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis

Latex:
\mforall{}P,f:Top.    (bag-mapfilter(f;P;\{\})  \msim{}  \{\})



Date html generated: 2016_05_15-PM-02_23_50
Last ObjectModification: 2015_12_27-AM-09_53_50

Theory : bags


Home Index