This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )