### Nuprl Lemma : isect2_decomp

`∀[t1,t2:Type]. ∀[x:t1 ⋂ t2].  ((x ∈ t1) ∧ (x ∈ t2))`

Proof

Definitions occuring in Statement :  isect2: `T1 ⋂ T2` uall: `∀[x:A]. B[x]` and: `P ∧ Q` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` isect2: `T1 ⋂ T2` btrue: `tt` ifthenelse: `if b then t else f fi ` guard: `{T}` subtype_rel: `A ⊆r B` bfalse: `ff`
Lemmas referenced :  isect2_wf subtype_rel_self btrue_wf bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation hypothesis sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  extract_by_obid isectElimination hypothesisEquality isect_memberEquality because_Cache Error :inhabitedIsType,  universeEquality applyEquality

Latex:
\mforall{}[t1,t2:Type].  \mforall{}[x:t1  \mcap{}  t2].    ((x  \mmember{}  t1)  \mwedge{}  (x  \mmember{}  t2))

Date html generated: 2019_06_20-AM-11_32_09
Last ObjectModification: 2018_09_26-AM-11_28_14

Theory : bool_1

Home Index