Nuprl Lemma : ringeq_int_terms_functionality

[r:Rng]. ∀[x1,x2,y1,y2:int_term()].  (uiff(x1 ≡ y1;x2 ≡ y2)) supposing (y1 ≡ y2 and x1 ≡ x2)


Definitions occuring in Statement :  ringeq_int_terms: t1 ≡ t2 rng: Rng int_term: int_term() uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  prop: rng: Rng all: x:A. B[x] ringeq_int_terms: t1 ≡ t2 and: P ∧ Q uiff: uiff(P;Q) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] implies:  Q rev_implies:  Q iff: ⇐⇒ Q guard: {T} subtype_rel: A ⊆B true: True squash: T
Lemmas referenced :  rng_wf int_term_wf ringeq_int_terms_wf rng_car_wf iff_weakening_equal ring_term_value_wf true_wf squash_wf equal_wf
Rules used in proof :  equalitySymmetry equalityTransitivity isect_memberEquality independent_pairEquality productElimination rename setElimination isectElimination extract_by_obid intEquality functionEquality axiomEquality hypothesisEquality thin dependent_functionElimination lambdaEquality sqequalRule because_Cache hypothesis lambdaFormation sqequalHypSubstitution independent_pairFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_functionElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality functionExtensionality universeEquality imageElimination applyEquality

\mforall{}[r:Rng].  \mforall{}[x1,x2,y1,y2:int\_term()].    (uiff(x1  \mequiv{}  y1;x2  \mequiv{}  y2))  supposing  (y1  \mequiv{}  y2  and  x1  \mequiv{}  x2)

Date html generated: 2018_05_21-PM-03_15_53
Last ObjectModification: 2018_01_25-PM-01_30_08

Theory : rings_1

Home Index