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

Theorem elrnmpt 5029
Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
Hypothesis
Ref Expression
rnmpt.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
elrnmpt  |-  ( C  e.  V  ->  ( C  e.  ran  F  <->  E. x  e.  A  C  =  B ) )
Distinct variable group:    x, C
Allowed substitution hints:    A( x)    B( x)    F( x)    V( x)

Proof of Theorem elrnmpt
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2372 . . 3  |-  ( y  =  C  ->  (
y  =  B  <->  C  =  B ) )
21rexbidv 2649 . 2  |-  ( y  =  C  ->  ( E. x  e.  A  y  =  B  <->  E. x  e.  A  C  =  B ) )
3 rnmpt.1 . . 3  |-  F  =  ( x  e.  A  |->  B )
43rnmpt 5028 . 2  |-  ran  F  =  { y  |  E. x  e.  A  y  =  B }
52, 4elab2g 3001 1  |-  ( C  e.  V  ->  ( C  e.  ran  F  <->  E. x  e.  A  C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1647    e. wcel 1715   E.wrex 2629    e. cmpt 4179   ran crn 4793
This theorem is referenced by:  elrnmpt1s  5030  onnseq  6503  oarec  6702  fifo  7332  infpwfien  7836  fin23lem38  8122  fin1a2lem13  8185  ac6num  8253  isercoll2  12349  iserodd  13096  gsumwspan  14678  odf1o2  15094  ordtbas2  17138  ordtopn1  17141  ordtopn2  17142  pnfnei  17167  mnfnei  17168  pnrmcld  17287  2ndcomap  17401  dis2ndc  17403  ptpjopn  17523  fbasrn  17792  elfm  17855  rnelfmlem  17860  rnelfm  17861  fmfnfmlem3  17864  fmfnfmlem4  17865  fmfnfm  17866  ptcmplem2  17960  tsmsfbas  18023  imasdsf1olem  18150  xpsdsval  18158  met1stc  18280  xrtgioo  18525  minveclem3b  19007  uniioombllem3  19155  dvivth  19572  ustuqtoplem  23863  utopsnneiplem  23871  fmucnd  23906  metustel  23914  metustsym  23919  metustbl  23930  restmetu  23935  esumcst  24041  measdivcstOLD  24162  measdivcst  24163  cvmsss2  24529  itg2addnclem2  25761  stoweidlem27  27367  stoweidlem31  27371  stoweidlem35  27375  stirlinglem5  27418  stirlinglem13  27426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pr 4316
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-opab 4180  df-mpt 4181  df-cnv 4800  df-dm 4802  df-rn 4803
  Copyright terms: Public domain W3C validator