Nuprl Lemma : rsub_functionality

[x1,x2,y1,y2:ℝ].  ((x1 y1) (x2 y2)) supposing ((y1 y2) and (x1 x2))


Definitions occuring in Statement :  rsub: y req: y real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rsub: y implies:  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

\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