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	\|- 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