breldmg

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

		Ref	Expression
	Assertion	breldmg	$⊢ (A \in C \land B \in D \land A R B) \to A \in dom R$

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = B \to (A R x \leftrightarrow A R B)$
2	1	spcegv	$⊢ B \in D \to (A R B \to \exists x A R x)$
3	2	imp	$⊢ (B \in D \land A R B) \to \exists x A R x$
4		eldmg	$⊢ A \in C \to (A \in dom R \leftrightarrow \exists x A R x)$
5	3 4	imbitrrid	$⊢ A \in C \to ((B \in D \land A R B) \to A \in dom R)$
6	5	3impib	$⊢ (A \in C \land B \in D \land A R B) \to A \in dom R$

Metamath Proof Explorer