Nuprl Lemma : rneq_functionality

x1,x2,y1,y2:ℝ.  (x1 ≠ y1 ⇐⇒ x2 ≠ y2) supposing ((y1 y2) and (x1 x2))


Definitions occuring in Statement :  rneq: x ≠ y req: y real: uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] implies:  Q rneq: x ≠ y prop: iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q or: P ∨ Q
Lemmas referenced :  req_witness req_wf real_wf or_wf rless_wf iff_wf rless_functionality req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis rename independent_pairFormation because_Cache addLevel productElimination impliesFunctionality orFunctionality dependent_functionElimination independent_isectElimination orLevelFunctionality

\mforall{}x1,x2,y1,y2:\mBbbR{}.    (x1  \mneq{}  y1  \mLeftarrow{}{}\mRightarrow{}  x2  \mneq{}  y2)  supposing  ((y1  =  y2)  and  (x1  =  x2))

Date html generated: 2016_05_18-AM-07_10_32
Last ObjectModification: 2015_12_28-AM-00_38_44

Theory : reals

Home Index