Theorem breldm

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995)

	Ref	Expression
Hypotheses	opeldm.1	⊢ 𝐴 ∈ V
	opeldm.2	⊢ 𝐵 ∈ V
Assertion	breldm	⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		opeldm.1	⊢ 𝐴 ∈ V
2		opeldm.2	⊢ 𝐵 ∈ V
3		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
4	1 2	opeldm	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅 )
5	3 4	sylbi	⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ dom 𝑅 )