Theorem brelrng

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

	Ref	Expression
Assertion	brelrng	|- ( ( A e. F /\ B e. G /\ A C B ) -> B e. ran C )

Proof

Step	Hyp	Ref	Expression
1		brcnvg	|- ( ( B e. G /\ A e. F ) -> ( B `' C A <-> A C B ) )
2	1	ancoms	|- ( ( A e. F /\ B e. G ) -> ( B `' C A <-> A C B ) )
3	2	biimp3ar	|- ( ( A e. F /\ B e. G /\ A C B ) -> B `' C A )
4		breldmg	|- ( ( B e. G /\ A e. F /\ B `' C A ) -> B e. dom `' C )
5	4	3com12	|- ( ( A e. F /\ B e. G /\ B `' C A ) -> B e. dom `' C )
6	3 5	syld3an3	|- ( ( A e. F /\ B e. G /\ A C B ) -> B e. dom `' C )
7		df-rn	|- ran C = dom `' C
8	6 7	eleqtrrdi	|- ( ( A e. F /\ B e. G /\ A C B ) -> B e. ran C )