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	⊢ ( ⟨ 𝐴 , 0R ⟩ ∈ ℝ ↔ 𝐴 ∈ R )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 0R = 0R
2		df-r	⊢ ℝ = ( R × { 0R } )
3	2	eleq2i	⊢ ( ⟨ 𝐴 , 0R ⟩ ∈ ℝ ↔ ⟨ 𝐴 , 0R ⟩ ∈ ( R × { 0R } ) )
4		opelxp	⊢ ( ⟨ 𝐴 , 0R ⟩ ∈ ( R × { 0R } ) ↔ ( 𝐴 ∈ R ∧ 0R ∈ { 0R } ) )
5		0r	⊢ 0R ∈ R
6	5	elexi	⊢ 0R ∈ V
7	6	elsn	⊢ ( 0R ∈ { 0R } ↔ 0R = 0R )
8	7	anbi2i	⊢ ( ( 𝐴 ∈ R ∧ 0R ∈ { 0R } ) ↔ ( 𝐴 ∈ R ∧ 0R = 0R ) )
9	3 4 8	3bitri	⊢ ( ⟨ 𝐴 , 0R ⟩ ∈ ℝ ↔ ( 𝐴 ∈ R ∧ 0R = 0R ) )
10	1 9	mpbiran2	⊢ ( ⟨ 𝐴 , 0R ⟩ ∈ ℝ ↔ 𝐴 ∈ R )