Metamath Proof Explorer

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 = { x | x

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1p 
 |-  1P
1 vx 
 |-  x
2 1 cv 
 |-  x
3 cltq 
 |-
4 c1q 
 |-  1Q
5 2 4 3 wbr 
 |-  x
6 5 1 cab 
 |-  { x | x
7 0 6 wceq 
 |-  1P = { x | x