Theorem 1pr

Description: The positive real number 'one'. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	1pr	|- 1P e. P.

Proof

Step	Hyp	Ref	Expression
1		df-1p	|- 1P = { x | x
2		1nq	|- 1Q e. Q.
3		nqpr	|- ( 1Q e. Q. -> { x | x
4	2 3	ax-mp	|- { x | x
5	1 4	eqeltri	|- 1P e. P.