Nuprl Lemma : seteq_functionality
∀x1,x2,y1,y2:coSet{i:l}.  (seteq(x1;x2) 
⇒ seteq(y1;y2) 
⇒ (seteq(x1;y1) 
⇐⇒ seteq(x2;y2)))
Proof
Definitions occuring in Statement : 
seteq: seteq(s1;s2)
, 
coSet: coSet{i:l}
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
Definitions unfolded in proof : 
rev_implies: P 
⇐ Q
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
guard: {T}
, 
member: t ∈ T
, 
and: P ∧ Q
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
Lemmas referenced : 
coSet_wf, 
seteq_wf, 
seteq_transitivity, 
seteq_inversion
Rules used in proof : 
isectElimination, 
hypothesis, 
independent_functionElimination, 
hypothesisEquality, 
thin, 
dependent_functionElimination, 
sqequalHypSubstitution, 
extract_by_obid, 
introduction, 
cut, 
independent_pairFormation, 
lambdaFormation, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution
Latex:
\mforall{}x1,x2,y1,y2:coSet\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(y1;y2)  {}\mRightarrow{}  (seteq(x1;y1)  \mLeftarrow{}{}\mRightarrow{}  seteq(x2;y2)))
Date html generated:
2018_07_29-AM-09_51_26
Last ObjectModification:
2018_07_11-PM-00_18_02
Theory : constructive!set!theory
Home
Index