Metamath Proof Explorer

Theorem relelrn

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

Ref Expression
Assertion relelrn 
|- ( ( Rel R /\ A R B ) -> B e. ran R )

Proof

Step Hyp Ref Expression
1 brrelex1 
 |-  ( ( Rel R /\ A R B ) -> A e. _V )
2 brrelex2 
 |-  ( ( Rel R /\ A R B ) -> B e. _V )
3 simpr 
 |-  ( ( Rel R /\ A R B ) -> A R B )
4 brelrng 
 |-  ( ( A e. _V /\ B e. _V /\ A R B ) -> B e. ran R )
5 1 2 3 4 syl3anc 
 |-  ( ( Rel R /\ A R B ) -> B e. ran R )