Theorem elreal

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

	Ref	Expression
Assertion	elreal	⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-r	⊢ ℝ = ( R × { 0R } )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℝ ↔ 𝐴 ∈ ( R × { 0R } ) )
3		elxp2	⊢ ( 𝐴 ∈ ( R × { 0R } ) ↔ ∃ 𝑥 ∈ R ∃ 𝑦 ∈ { 0R } 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
4		0r	⊢ 0R ∈ R
5	4	elexi	⊢ 0R ∈ V
6		opeq2	⊢ ( 𝑦 = 0R → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 0R ⟩ )
7	6	eqeq2d	⊢ ( 𝑦 = 0R → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 0R ⟩ ) )
8	5 7	rexsn	⊢ ( ∃ 𝑦 ∈ { 0R } 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 0R ⟩ )
9		eqcom	⊢ ( 𝐴 = ⟨ 𝑥 , 0R ⟩ ↔ ⟨ 𝑥 , 0R ⟩ = 𝐴 )
10	8 9	bitri	⊢ ( ∃ 𝑦 ∈ { 0R } 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 0R ⟩ = 𝐴 )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ R ∃ 𝑦 ∈ { 0R } 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
12	3 11	bitri	⊢ ( 𝐴 ∈ ( R × { 0R } ) ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
13	2 12	bitri	⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )