Nuprl Lemma : orderedpair-fst_functionality

a,b:coSet{i:l}.  (seteq(a;b)  seteq(fst(a);fst(b)))


Proof




Definitions occuring in Statement :  orderedpair-fst: fst(pr) seteq: seteq(s1;s2) coSet: coSet{i:l} all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  prop: rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q uall: [x:A]. B[x] member: t ∈ T orderedpair-fst: fst(pr) implies:  Q all: x:A. B[x]
Lemmas referenced :  coSet_wf seteq_wf seteq_weakening orderedpair-fsts_functionality singleitem_functionality orderedpair-fsts_wf singleitem_wf seteq_functionality
Rules used in proof :  productElimination independent_functionElimination because_Cache hypothesis hypothesisEquality isectElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut sqequalRule lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a,b:coSet\{i:l\}.    (seteq(a;b)  {}\mRightarrow{}  seteq(fst(a);fst(b)))



Date html generated: 2018_07_29-AM-10_02_06
Last ObjectModification: 2018_07_18-PM-03_04_35

Theory : constructive!set!theory


Home Index