This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Detailed syntax breakdown

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