Nuprl Lemma : union_empty_lemma

b,eq:Top.  (b ⋃ {} b)


Proof




Definitions occuring in Statement :  empty-fset: {} fset-union: x ⋃ y top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T empty-fset: {} fset-union: x ⋃ y l-union: as ⋃ bs top: Top
Lemmas referenced :  top_wf reduce_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}b,eq:Top.    (b  \mcup{}  \{\}  \msim{}  b)



Date html generated: 2016_05_14-PM-03_45_50
Last ObjectModification: 2015_12_26-PM-06_37_35

Theory : finite!sets


Home Index