Metamath Proof Explorer

Theorem breldmg

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007)

Ref Expression
Assertion breldmg ⊢ A ∈ C ∧ B ∈ D ∧ A R B → A ∈ dom ⁡ R

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = B → A R x ↔ A R B
2 1 spcegv ⊢ B ∈ D → A R B → ∃ x A R x
3 2 imp ⊢ B ∈ D ∧ A R B → ∃ x A R x
4 eldmg ⊢ A ∈ C → A ∈ dom ⁡ R ↔ ∃ x A R x
5 3 4 imbitrrid ⊢ A ∈ C → B ∈ D ∧ A R B → A ∈ dom ⁡ R
6 5 3impib ⊢ A ∈ C ∧ B ∈ D ∧ A R B → A ∈ dom ⁡ R