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

Metamath Proof Explorer

Theorem eldmg

Description: Domain membership. Theorem 4 of Suppes p. 59. (Contributed by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion eldmg ⊢ A ∈ V → A ∈ dom ⁡ B ↔ ∃ y A B y

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = A → x B y ↔ A B y
2 1 exbidv ⊢ x = A → ∃ y x B y ↔ ∃ y A B y
3 df-dm ⊢ dom ⁡ B = x | ∃ y x B y
4 2 3 elab2g ⊢ A ∈ V → A ∈ dom ⁡ B ↔ ∃ y A B y