Theorem 0r

Description: The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	0r	|- 0R e. R.

Proof

Step	Hyp	Ref	Expression
1		1pr	|- 1P e. P.
2		opelxpi	|- ( ( 1P e. P. /\ 1P e. P. ) -> <. 1P , 1P >. e. ( P. X. P. ) )
3	1 1 2	mp2an	|- <. 1P , 1P >. e. ( P. X. P. )
4		enrex	|- ~R e. _V
5	4	ecelqsi	|- ( <. 1P , 1P >. e. ( P. X. P. ) -> [ <. 1P , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
6	3 5	ax-mp	|- [ <. 1P , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R )
7		df-0r	|- 0R = [ <. 1P , 1P >. ] ~R
8		df-nr	|- R. = ( ( P. X. P. ) /. ~R )
9	6 7 8	3eltr4i	|- 0R e. R.