Nuprl Lemma : rneq-symmetry
∀x,y:ℝ. (x ≠ y ⇒ y ≠ x)
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
rneq: x ≠ y,
or: P ∨ Q,
guard: {T},
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rless_wf,
rneq_wf,
real_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
unionElimination,
thin,
sqequalRule,
cut,
hypothesis,
inrFormation,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
inlFormation
Latex:
\mforall{}x,y:\mBbbR{}. (x \mneq{} y {}\mRightarrow{} y \mneq{} x)
Date html generated:
2016_10_26-AM-09_08_04
Last ObjectModification:
2016_10_14-PM-05_45_59
Theory : reals
Home
Index