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

Metamath Proof Explorer

Theorem breldmd

Description: Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses breldmd.1 ⊢ φ → A ∈ C
breldmd.2 ⊢ φ → B ∈ D
breldmd.3 ⊢ φ → A R B
Assertion breldmd ⊢ φ → A ∈ dom ⁡ R

Proof

Step Hyp Ref Expression
1 breldmd.1 ⊢ φ → A ∈ C
2 breldmd.2 ⊢ φ → B ∈ D
3 breldmd.3 ⊢ φ → A R B
4 breldmg ⊢ A ∈ C ∧ B ∈ D ∧ A R B → A ∈ dom ⁡ R
5 1 2 3 4 syl3anc ⊢ φ → A ∈ dom ⁡ R