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

Theorem fvelrnb 5919
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 5918 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21eleq2d 2490 . 2  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) } ) )
3 fvex 5882 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2492 . . . . 5  |-  ( ( F `  x )  =  B  ->  (
( F `  x
)  e.  _V  <->  B  e.  _V ) )
53, 4mpbii 214 . . . 4  |-  ( ( F `  x )  =  B  ->  B  e.  _V )
65rexlimivw 2912 . . 3  |-  ( E. x  e.  A  ( F `  x )  =  B  ->  B  e.  _V )
7 eqeq1 2424 . . . . 5  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  B  =  ( F `  x ) ) )
8 eqcom 2429 . . . . 5  |-  ( B  =  ( F `  x )  <->  ( F `  x )  =  B )
97, 8syl6bb 264 . . . 4  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  ( F `  x )  =  B ) )
109rexbidv 2937 . . 3  |-  ( y  =  B  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  ( F `  x )  =  B ) )
116, 10elab3 3222 . 2  |-  ( B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) }  <->  E. x  e.  A  ( F `  x )  =  B )
122, 11syl6bb 264 1  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1867   {cab 2405   E.wrex 2774   _Vcvv 3078   ran crn 4846    Fn wfn 5587   ` cfv 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5556  df-fun 5594  df-fn 5595  df-fv 5600
This theorem is referenced by:  foelrni  5920  chfnrn  5999  rexrn  6030  ralrn  6031  elrnrexdmb  6033  ffnfv  6055  fconstfvOLD  6133  elunirn  6162  isoini  6235  canth  6255  reldm  6849  seqomlem2  7167  fipreima  7877  ordiso2  8021  inf0  8117  inf3lem6  8129  noinfep  8155  cantnflem4  8187  infenaleph  8511  isinfcard  8512  dfac5  8548  ackbij1  8657  sornom  8696  fin23lem16  8754  fin23lem21  8758  isf32lem2  8773  fin1a2lem5  8823  itunitc  8840  axdc3lem2  8870  zorn2lem4  8918  cfpwsdom  8998  peano2nn  10610  uzn0  11163  om2uzrani  12152  uzrdgfni  12158  uzin2  13375  unbenlem  14804  vdwlem6  14888  0ram  14930  imasmnd2  16517  imasgrp2  16745  pmtrfrn  17043  pgpssslw  17194  efgsfo  17317  efgrelexlemb  17328  gexex  17419  imasring  17775  mpfind  18687  mpfpf1  18867  pf1mpf  18868  lindfrn  19303  2ndcomap  20397  kgenidm  20486  kqreglem1  20680  zfbas  20835  rnelfmlem  20891  rnelfm  20892  fmfnfmlem2  20894  ovolctb  22317  ovolicc2  22350  mbfinf  22495  mbfinfOLD  22496  dvivth  22836  dvne0  22837  aannenlem3  23148  reeff1o  23264  usgraedgrn  24951  usgra2edg  24952  usgrarnedg  24954  vdn0frgrav2  25593  vdgn0frgrav2  25594  rnbra  27592  cnvbraval  27595  pjssdif1i  27660  dfpjop  27667  elpjrn  27675  foresf1o  27972  esumfsup  28727  esumiun  28751  msrid  29968  ghomgrpilem2  30089  tailfb  30815  indexdom  31765  cdleme50rnlem  33820  diaelrnN  34322  diaintclN  34335  cdlemm10N  34395  dibintclN  34444  dihglb2  34619  dihintcl  34621  lcfrlem9  34827  mapd1o  34925  hdmaprnlem11N  35140  hgmaprnlem4N  35179  nacsfix  35263  fvelrnbf  36983  cncmpmax  36997  stoweidlem27  37460  stoweidlem31  37465  stoweidlem48  37482  stoweidlem59  37493  stirlinglem13  37521  fourierdlem12  37554  fourierdlem41  37583  fourierdlem42  37584  fourierdlem46  37588  fourierdlem48  37590  fourierdlem49  37591  fourierdlem70  37612  fourierdlem71  37613  fourierdlem74  37616  fourierdlem75  37617  fourierdlem102  37644  fourierdlem103  37645  fourierdlem104  37646  fourierdlem114  37656  sge0tsms  37760  sge0sup  37771  sge0le  37787  nnfoctbdjlem  37806  meadjiunlem  37816  iccpartrn  38147  iccpartnel  38155
  Copyright terms: Public domain W3C validator