Nuprl Lemma : orderedpair-fsts_wf

[pr:coSet{i:l}]. (orderedpair-fsts(pr) ∈ coSet{i:l})


Proof




Definitions occuring in Statement :  orderedpair-fsts: orderedpair-fsts(pr) coSet: coSet{i:l} uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  orderedpair-fsts: orderedpair-fsts(pr) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  coSet_wf intersectionset_wf
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:coSet\{i:l\}].  (orderedpair-fsts(pr)  \mmember{}  coSet\{i:l\})



Date html generated: 2018_07_29-AM-10_01_49
Last ObjectModification: 2018_07_18-PM-02_58_56

Theory : constructive!set!theory


Home Index