This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⟩ = 𝐴 )