brelrng

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008)

		Ref	Expression
	Assertion	brelrng	$⊢ (A \in F \land B \in G \land A C B) \to B \in ran C$

Step	Hyp	Ref	Expression
1		brcnvg	$⊢ (B \in G \land A \in F) \to (B C^{-1} A \leftrightarrow A C B)$
2	1	ancoms	$⊢ (A \in F \land B \in G) \to (B C^{-1} A \leftrightarrow A C B)$
3	2	biimp3ar	$⊢ (A \in F \land B \in G \land A C B) \to B C^{-1} A$
4		breldmg	$⊢ (B \in G \land A \in F \land B C^{-1} A) \to B \in dom C^{-1}$
5	4	3com12	$⊢ (A \in F \land B \in G \land B C^{-1} A) \to B \in dom C^{-1}$
6	3 5	syld3an3	$⊢ (A \in F \land B \in G \land A C B) \to B \in dom C^{-1}$
7		df-rn	$⊢ ran C = dom C^{-1}$
8	6 7	eleqtrrdi	$⊢ (A \in F \land B \in G \land A C B) \to B \in ran C$

Metamath Proof Explorer