Nuprl Lemma : req*_functionality
∀[x1,x2,y1,y2:ℝ*]. (x1 = x2 ⇒ y1 = y2 ⇒ (x1 = y1 ⇐⇒ x2 = y2))
Proof
Definitions occuring in Statement :
req*: x = y,
real*: ℝ*,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q
Lemmas referenced :
req*_wf,
real*_wf,
req*_transitivity,
req*_inversion
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
independent_pairFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_functionElimination,
because_Cache
Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}*]. (x1 = x2 {}\mRightarrow{} y1 = y2 {}\mRightarrow{} (x1 = y1 \mLeftarrow{}{}\mRightarrow{} x2 = y2))
Date html generated:
2018_05_22-PM-03_14_38
Last ObjectModification:
2017_10_06-PM-02_09_21
Theory : reals_2
Home
Index