Axiom ax-pre-ltirr 7991

Description: Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7991. (Contributed by Jim Kingdon, 12-Jan-2020.)

Assertion

Ref	Expression
ax-pre-ltirr	|- ( A e. RR -> -. A <RR A )

Detailed syntax breakdown of Axiom ax-pre-ltirr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cr 7878	. . 3 class RR
3	1, 2	wcel 2167	. 2 wff A e. RR
4		cltrr 7883	. . . 4 class <RR
5	1, 1, 4	wbr 4033	. . 3 wff A <RR A
6	5	wn 3	. 2 wff -. A <RR A
7	3, 6	wi 4	1 wff ( A e. RR -> -. A <RR A )

This axiom is referenced by:  axltirr  8093