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	$$⊢1_{𝑷}=\left\{x|x{<}_{𝑸}{1}_{𝑸}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1p	$$class{1}_{𝑷}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3		cltq	$$class{<}_{𝑸}$$
4		c1q	$$class{1}_{𝑸}$$
5	2 4 3	wbr	$$wffx{<}_{𝑸}{1}_{𝑸}$$
6	5 1	cab	$$class\left\{x|x{<}_{𝑸}{1}_{𝑸}\right\}$$
7	0 6	wceq	$$wff{1}_{𝑷}=\left\{x|x{<}_{𝑸}{1}_{𝑸}\right\}$$