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

Theorem brelrn 5159
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 5158 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V  /\  A C B )  ->  B  e.  ran  C )
41, 2, 3mp3an12 1312 1  |-  ( A C B  ->  B  e.  ran  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836   _Vcvv 3047   class class class wbr 4380   ran crn 4927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-br 4381  df-opab 4439  df-cnv 4934  df-dm 4936  df-rn 4937
This theorem is referenced by:  opelrn  5160  dfco2a  5428  cores  5431  dffun9  5537  funcnv  5569  rntpos  6904  aceq3lem  8432  axdclem  8830  axdclem2  8831  cotr2g  12833  shftfval  12924  psdmrn  15973  metustexhalfOLD  21170  metustexhalf  21171  itg1addlem4  22210
  Copyright terms: Public domain W3C validator