Theorem opelreal

Description: Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	opelreal	|- ( <. A , 0R >. e. RR <-> A e. R. )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- 0R = 0R
2		df-r	|- RR = ( R. X. { 0R } )
3	2	eleq2i	|- ( <. A , 0R >. e. RR <-> <. A , 0R >. e. ( R. X. { 0R } ) )
4		opelxp	|- ( <. A , 0R >. e. ( R. X. { 0R } ) <-> ( A e. R. /\ 0R e. { 0R } ) )
5		0r	|- 0R e. R.
6	5	elexi	|- 0R e. _V
7	6	elsn	|- ( 0R e. { 0R } <-> 0R = 0R )
8	7	anbi2i	|- ( ( A e. R. /\ 0R e. { 0R } ) <-> ( A e. R. /\ 0R = 0R ) )
9	3 4 8	3bitri	|- ( <. A , 0R >. e. RR <-> ( A e. R. /\ 0R = 0R ) )
10	1 9	mpbiran2	|- ( <. A , 0R >. e. RR <-> A e. R. )