Theorem opelcn

Description: Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	opelcn	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ℂ ↔ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )

Proof

Step	Hyp	Ref	Expression
1		df-c	⊢ ℂ = ( R × R )
2	1	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ℂ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( R × R ) )
3		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( R × R ) ↔ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )
4	2 3	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ℂ ↔ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )