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

Theorem fvelrnb 5775
Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)
Assertion
Ref Expression
fvelrnb  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  B ) )
Distinct variable groups:    x, A    x, B    x, F

Proof of Theorem fvelrnb
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 fnrnfv 5774 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21eleq2d 2504 . 2  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) } ) )
3 fvex 5743 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2497 . . . . 5  |-  ( ( F `  x )  =  B  ->  (
( F `  x
)  e.  _V  <->  B  e.  _V ) )
53, 4mpbii 204 . . . 4  |-  ( ( F `  x )  =  B  ->  B  e.  _V )
65rexlimivw 2827 . . 3  |-  ( E. x  e.  A  ( F `  x )  =  B  ->  B  e.  _V )
7 eqeq1 2443 . . . . 5  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  B  =  ( F `  x ) ) )
8 eqcom 2439 . . . . 5  |-  ( B  =  ( F `  x )  <->  ( F `  x )  =  B )
97, 8syl6bb 254 . . . 4  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  ( F `  x )  =  B ) )
109rexbidv 2727 . . 3  |-  ( y  =  B  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  ( F `  x )  =  B ) )
116, 10elab3 3090 . 2  |-  ( B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) }  <->  E. x  e.  A  ( F `  x )  =  B )
122, 11syl6bb 254 1  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   {cab 2423   E.wrex 2707   _Vcvv 2957   ran crn 4880    Fn wfn 5450   ` cfv 5455
This theorem is referenced by:  chfnrn  5842  rexrn  5873  ralrn  5874  elrnrexdmb  5876  ffnfv  5895  fconstfv  5955  elunirnALT  6001  isoini  6059  reldm  6399  canth  6540  seqomlem2  6709  fipreima  7413  ordiso2  7485  inf0  7577  inf3lem6  7589  noinfep  7615  noinfepOLD  7616  cantnflem4  7649  infenaleph  7973  isinfcard  7974  dfac5  8010  ackbij1  8119  sornom  8158  fin23lem16  8216  fin23lem21  8220  isf32lem2  8235  fin1a2lem5  8285  itunitc  8302  axdc3lem2  8332  zorn2lem4  8380  cfpwsdom  8460  peano2nn  10013  uzn0  10502  om2uzrani  11293  uzrdgfni  11299  uzin2  12149  unbenlem  13277  vdwlem6  13355  0ram  13389  imasmnd2  14733  imasgrp2  14934  pgpssslw  15249  efgsfo  15372  efgrelexlemb  15383  gexex  15469  imasrng  15726  bwth  17474  2ndcomap  17522  kgenidm  17580  kqreglem1  17774  zfbas  17929  rnelfmlem  17985  rnelfm  17986  fmfnfmlem2  17988  ovolctb  19387  ovolicc2  19419  mbfinf  19558  dvivth  19895  dvne0  19896  mpfind  19966  mpfpf1  19972  pf1mpf  19973  aannenlem3  20248  reeff1o  20364  usgraedgrn  21402  usgra2edg  21403  usgrarnedg  21405  rnbra  23611  cnvbraval  23614  pjssdif1i  23679  dfpjop  23686  elpjrn  23694  esumfsup  24461  ghomgrpilem2  25098  tailfb  26407  indexdom  26437  nacsfix  26767  lindfrn  27269  pmtrfrn  27378  fvelrnbf  27666  cncmpmax  27680  stoweidlem27  27753  stoweidlem31  27757  stoweidlem48  27774  stoweidlem59  27785  stirlinglem13  27812  vdn0frgrav2  28415  vdgn0frgrav2  28416  cdleme50rnlem  31342  diaelrnN  31844  diaintclN  31857  cdlemm10N  31917  dibintclN  31966  dihglb2  32141  dihintcl  32143  lcfrlem9  32349  mapd1o  32447  hdmaprnlem11N  32662  hgmaprnlem4N  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pr 4404
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-sbc 3163  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-mpt 4269  df-id 4499  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-iota 5419  df-fun 5457  df-fn 5458  df-fv 5463
  Copyright terms: Public domain W3C validator