Nuprl Lemma : rneq_irrefl
∀[e:ℝ]. (¬e ≠ e)
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
real: ℝ,
uall: ∀[x:A]. B[x],
not: ¬A
Definitions unfolded in proof :
prop: ℙ,
uimplies: b supposing a,
false: False,
implies: P ⇒ Q,
not: ¬A,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
real_wf,
rneq_wf,
rneq_irreflexivity
Rules used in proof :
dependent_functionElimination,
lambdaEquality,
sqequalRule,
independent_functionElimination,
because_Cache,
voidElimination,
hypothesis,
independent_isectElimination,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
thin,
lambdaFormation,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[e:\mBbbR{}]. (\mneg{}e \mneq{} e)
Date html generated:
2018_07_29-AM-09_39_44
Last ObjectModification:
2018_06_29-PM-00_07_56
Theory : reals
Home
Index