MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brelrn Unicode version

Theorem brelrn 4909
Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
Hypotheses
Ref Expression
brelrn.1  |-  A  e. 
_V
brelrn.2  |-  B  e. 
_V
Assertion
Ref Expression
brelrn  |-  ( A C B  ->  B  e.  ran  C )

Proof of Theorem brelrn
StepHypRef Expression
1 brelrn.1 . 2  |-  A  e. 
_V
2 brelrn.2 . 2  |-  B  e. 
_V
3 brelrng 4908 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V  /\  A C B )  ->  B  e.  ran  C )
41, 2, 3mp3an12 1267 1  |-  ( A C B  ->  B  e.  ran  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   _Vcvv 2788   class class class wbr 4023   ran crn 4690
This theorem is referenced by:  opelrn  4910  dfco2a  5173  cores  5176  dffun9  5282  funcnv  5310  rntpos  6247  aceq3lem  7747  axdclem  8146  axdclem2  8147  shftfval  11565  psdmrn  14316  itg1addlem4  19054  ranfldrefc  25058  domrngref  25060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700
  Copyright terms: Public domain W3C validator