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

Metamath Proof Explorer

Theorem eldm4

Description: Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018)

Ref Expression
Assertion eldm4 ⊢ A ∈ V → A ∈ dom ⁡ R ↔ ∃ y y ∈ A R

Proof

Step Hyp Ref Expression
1 eldmg ⊢ A ∈ V → A ∈ dom ⁡ R ↔ ∃ y A R y
2 elecALTV ⊢ A ∈ V ∧ y ∈ V → y ∈ A R ↔ A R y
3 2 elvd ⊢ A ∈ V → y ∈ A R ↔ A R y
4 3 exbidv ⊢ A ∈ V → ∃ y y ∈ A R ↔ ∃ y A R y
5 1 4 bitr4d ⊢ A ∈ V → A ∈ dom ⁡ R ↔ ∃ y y ∈ A R