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