Nuprl Lemma : snd-orderedpairset

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


Proof




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

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



Date html generated: 2018_07_29-AM-10_02_34
Last ObjectModification: 2018_07_18-PM-03_17_17

Theory : constructive!set!theory


Home Index