### Nuprl Lemma : rsub_functionality

`∀[x1,x2,y1,y2:ℝ].  ((x1 - y1) = (x2 - y2)) supposing ((y1 = y2) and (x1 = x2))`

Proof

Definitions occuring in Statement :  rsub: `x - y` req: `x = y` real: `ℝ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` rsub: `x - y` implies: `P `` Q` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  req_witness rsub_wf req_wf real_wf radd_wf rminus_wf req_weakening req_functionality radd_functionality rminus_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry independent_isectElimination productElimination

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}].    ((x1  -  y1)  =  (x2  -  y2))  supposing  ((y1  =  y2)  and  (x1  =  x2))

Date html generated: 2016_05_18-AM-06_55_09
Last ObjectModification: 2015_12_28-AM-00_31_35

Theory : reals

Home Index