Nuprl Lemma : isect2_subtype_rel

[A,B:Type].  (A ⋂ B ⊆A)


Proof




Definitions occuring in Statement :  isect2: T1 ⋂ T2 subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B and: P ∧ Q cand: c∧ B
Lemmas referenced :  isect2_decomp isect2_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination equalityTransitivity hypothesis equalitySymmetry independent_pairFormation sqequalRule axiomEquality universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A,B:Type].    (A  \mcap{}  B  \msubseteq{}r  A)



Date html generated: 2016_05_13-PM-03_58_06
Last ObjectModification: 2015_12_26-AM-10_51_31

Theory : bool_1


Home Index