Metamath Proof Explorer

Theorem brelrn

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004)

Ref Expression
Hypotheses brelrn.1 
|- A e. _V
brelrn.2 
|- B e. _V
Assertion brelrn 
|- ( A C B -> B e. ran C )

Proof

Step Hyp Ref Expression
1 brelrn.1 
 |-  A e. _V
2 brelrn.2 
 |-  B e. _V
3 brelrng 
 |-  ( ( A e. _V /\ B e. _V /\ A C B ) -> B e. ran C )
4 1 2 3 mp3an12 
 |-  ( A C B -> B e. ran C )