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

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

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