ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-pre-ltirr GIF version

Axiom ax-pre-ltirr 7839
Description: Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7839. (Contributed by Jim Kingdon, 12-Jan-2020.)
Assertion
Ref Expression
ax-pre-ltirr (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)

Detailed syntax breakdown of Axiom ax-pre-ltirr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cr 7726 . . 3 class
31, 2wcel 2128 . 2 wff 𝐴 ∈ ℝ
4 cltrr 7731 . . . 4 class <
51, 1, 4wbr 3965 . . 3 wff 𝐴 < 𝐴
65wn 3 . 2 wff ¬ 𝐴 < 𝐴
73, 6wi 4 1 wff (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Colors of variables: wff set class
This axiom is referenced by:  axltirr  7939
  Copyright terms: Public domain W3C validator