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 ⊢ A ∈ ℝ ↔ ∃ x ∈ 𝑹 x 0 𝑹 = A

Proof

Step Hyp Ref Expression
1 df-r ⊢ ℝ = 𝑹 × 0 𝑹
2 1 eleq2i ⊢ A ∈ ℝ ↔ A ∈ 𝑹 × 0 𝑹
3 elxp2 ⊢ A ∈ 𝑹 × 0 𝑹 ↔ ∃ x ∈ 𝑹 ∃ y ∈ 0 𝑹 A = x y
4 0r ⊢ 0 𝑹 ∈ 𝑹
5 4 elexi ⊢ 0 𝑹 ∈ V
6 opeq2 ⊢ y = 0 𝑹 → x y = x 0 𝑹
7 6 eqeq2d ⊢ y = 0 𝑹 → A = x y ↔ A = x 0 𝑹
8 5 7 rexsn ⊢ ∃ y ∈ 0 𝑹 A = x y ↔ A = x 0 𝑹
9 eqcom ⊢ A = x 0 𝑹 ↔ x 0 𝑹 = A
10 8 9 bitri ⊢ ∃ y ∈ 0 𝑹 A = x y ↔ x 0 𝑹 = A
11 10 rexbii ⊢ ∃ x ∈ 𝑹 ∃ y ∈ 0 𝑹 A = x y ↔ ∃ x ∈ 𝑹 x 0 𝑹 = A
12 3 11 bitri ⊢ A ∈ 𝑹 × 0 𝑹 ↔ ∃ x ∈ 𝑹 x 0 𝑹 = A
13 2 12 bitri ⊢ A ∈ ℝ ↔ ∃ x ∈ 𝑹 x 0 𝑹 = A