Metamath Proof Explorer

Theorem releldmb

Description: Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015)

Ref Expression
Assertion releldmb ⊢ Rel ⁡ R → A ∈ dom ⁡ R ↔ ∃ x A R x

Proof

Step Hyp Ref Expression
1 eldmg ⊢ A ∈ dom ⁡ R → A ∈ dom ⁡ R ↔ ∃ x A R x
2 1 ibi ⊢ A ∈ dom ⁡ R → ∃ x A R x
3 releldm ⊢ Rel ⁡ R ∧ A R x → A ∈ dom ⁡ R
4 3 ex ⊢ Rel ⁡ R → A R x → A ∈ dom ⁡ R
5 4 exlimdv ⊢ Rel ⁡ R → ∃ x A R x → A ∈ dom ⁡ R
6 2 5 impbid2 ⊢ Rel ⁡ R → A ∈ dom ⁡ R ↔ ∃ x A R x