Nuprl Lemma : classical-and

[A,B:ℙ].  uiff({A} ∧ {B};{A ∧ B})


Proof




Definitions occuring in Statement :  classical: {P} uiff: uiff(P;Q) uall: [x:A]. B[x] prop: and: P ∧ Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a classical: {P} cand: c∧ B prop: unit: Unit
Lemmas referenced :  classical_wf and_wf it_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation sqequalHypSubstitution productElimination thin setElimination rename dependent_set_memberEquality lemma_by_obid hypothesis isectElimination hypothesisEquality because_Cache sqequalRule axiomEquality natural_numberEquality independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A,B:\mBbbP{}].    uiff(\{A\}  \mwedge{}  \{B\};\{A  \mwedge{}  B\})



Date html generated: 2016_05_13-PM-03_16_47
Last ObjectModification: 2016_01_06-PM-05_20_17

Theory : core_2


Home Index