Theorem breldmg

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

	Ref	Expression
Assertion	breldmg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥 ↔ 𝐴 𝑅 𝐵 ) )
2	1	spcegv	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 𝑅 𝐵 → ∃ 𝑥 𝐴 𝑅 𝑥 ) )
3	2	imp	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 𝑅 𝐵 ) → ∃ 𝑥 𝐴 𝑅 𝑥 )
4		eldmg	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
5	3 4	imbitrrid	⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 ) )
6	5	3impib	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )