Theorem elreal

Description: Membership in class of real numbers. (Contributed by NM, 31-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	elreal	|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )

Proof

Step	Hyp	Ref	Expression
1		df-r	|- RR = ( R. X. { 0R } )
2	1	eleq2i	|- ( A e. RR <-> A e. ( R. X. { 0R } ) )
3		elxp2	|- ( A e. ( R. X. { 0R } ) <-> E. x e. R. E. y e. { 0R } A = <. x , y >. )
4		0r	|- 0R e. R.
5	4	elexi	|- 0R e. _V
6		opeq2	|- ( y = 0R -> <. x , y >. = <. x , 0R >. )
7	6	eqeq2d	|- ( y = 0R -> ( A = <. x , y >. <-> A = <. x , 0R >. ) )
8	5 7	rexsn	|- ( E. y e. { 0R } A = <. x , y >. <-> A = <. x , 0R >. )
9		eqcom	|- ( A = <. x , 0R >. <-> <. x , 0R >. = A )
10	8 9	bitri	|- ( E. y e. { 0R } A = <. x , y >. <-> <. x , 0R >. = A )
11	10	rexbii	|- ( E. x e. R. E. y e. { 0R } A = <. x , y >. <-> E. x e. R. <. x , 0R >. = A )
12	3 11	bitri	|- ( A e. ( R. X. { 0R } ) <-> E. x e. R. <. x , 0R >. = A )
13	2 12	bitri	|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )