### Nuprl Lemma : rneq_functionality

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

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` req: `x = y` real: `ℝ` uimplies: `b supposing a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` rneq: `x ≠ y` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` 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

Latex:
\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