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	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	breldmd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	breldmd.3	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	breldmd	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		breldmd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		breldmd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		breldmd.3	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
4		breldmg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )