Nuprl Lemma : orderedpair-snd_wf2

[pr:Set{i:l}]. (snd(pr) ∈ Set{i:l})


Proof




Definitions occuring in Statement :  orderedpair-snd: snd(pr) Set: Set{i:l} uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  orderedpair-snd: snd(pr) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  Set_wf orderedpair-snds_wf2 singleitem_wf2
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[pr:Set\{i:l\}].  (snd(pr)  \mmember{}  Set\{i:l\})



Date html generated: 2018_07_29-AM-10_02_28
Last ObjectModification: 2018_07_18-PM-03_07_55

Theory : constructive!set!theory


Home Index