Axiom ax-1re 7868

Description: 1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7824. Proofs should use 1re 7919 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-1re	⊢ 1 ∈ ℝ

Detailed syntax breakdown of Axiom ax-1re

Step	Hyp	Ref	Expression
1		c1 7775	. 2 class 1
2		cr 7773	. 2 class ℝ
3	1, 2	wcel 2141	1 wff 1 ∈ ℝ

This axiom is referenced by:  1re  7919