Nuprl Lemma : b-union-equality-disjoint2

`∀A,B:Type. ∀a:A. ∀b:B.  ((a = b ∈ (A ⋃ B)) `` (¬¬A ⋂ B))`

Proof

Definitions occuring in Statement :  isect2: `T1 ⋂ T2` b-union: `A ⋃ B` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` not: `¬A` false: `False` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B`
Lemmas referenced :  b-union-equality-disjoint not_wf isect2_wf equal_wf b-union_wf subtype_rel_b-union-left subtype_rel_b-union-right
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination voidElimination isectElimination cumulativity applyEquality sqequalRule universeEquality

Latex:
\mforall{}A,B:Type.  \mforall{}a:A.  \mforall{}b:B.    ((a  =  b)  {}\mRightarrow{}  (\mneg{}\mneg{}A  \mcap{}  B))

Date html generated: 2016_05_13-PM-04_11_46
Last ObjectModification: 2015_12_26-AM-11_12_21

Theory : subtype_1

Home Index