Definition df-1p

Description: Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. Definition of Gleason p. 122. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-1p	⊢ 1P = { 𝑥 ∣ 𝑥 <Q 1Q }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1p	⊢ 1P
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		cltq	⊢ <Q
4		c1q	⊢ 1Q
5	2 4 3	wbr	⊢ 𝑥 <Q 1Q
6	5 1	cab	⊢ { 𝑥 ∣ 𝑥 <Q 1Q }
7	0 6	wceq	⊢ 1P = { 𝑥 ∣ 𝑥 <Q 1Q }