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

Theorem fvelrnb 5754
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 5753 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21eleq2d 2510 . 2  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) } ) )
3 fvex 5716 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2503 . . . . 5  |-  ( ( F `  x )  =  B  ->  (
( F `  x
)  e.  _V  <->  B  e.  _V ) )
53, 4mpbii 211 . . . 4  |-  ( ( F `  x )  =  B  ->  B  e.  _V )
65rexlimivw 2852 . . 3  |-  ( E. x  e.  A  ( F `  x )  =  B  ->  B  e.  _V )
7 eqeq1 2449 . . . . 5  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  B  =  ( F `  x ) ) )
8 eqcom 2445 . . . . 5  |-  ( B  =  ( F `  x )  <->  ( F `  x )  =  B )
97, 8syl6bb 261 . . . 4  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  ( F `  x )  =  B ) )
109rexbidv 2751 . . 3  |-  ( y  =  B  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  ( F `  x )  =  B ) )
116, 10elab3 3128 . 2  |-  ( B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) }  <->  E. x  e.  A  ( F `  x )  =  B )
122, 11syl6bb 261 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 184    = wceq 1369    e. wcel 1756   {cab 2429   E.wrex 2731   _Vcvv 2987   ran crn 4856    Fn wfn 5428   ` cfv 5433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-sbc 3202  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-iota 5396  df-fun 5435  df-fn 5436  df-fv 5441
This theorem is referenced by:  chfnrn  5829  rexrn  5860  ralrn  5861  elrnrexdmb  5863  ffnfv  5884  fconstfv  5955  elunirn  5983  isoini  6044  canth  6064  reldm  6640  seqomlem2  6921  fipreima  7632  ordiso2  7744  inf0  7842  inf3lem6  7854  noinfep  7880  noinfepOLD  7881  cantnflem4  7915  cantnflem4OLD  7937  infenaleph  8276  isinfcard  8277  dfac5  8313  ackbij1  8422  sornom  8461  fin23lem16  8519  fin23lem21  8523  isf32lem2  8538  fin1a2lem5  8588  itunitc  8605  axdc3lem2  8635  zorn2lem4  8683  cfpwsdom  8763  peano2nn  10349  uzn0  10891  om2uzrani  11790  uzrdgfni  11796  uzin2  12847  unbenlem  13984  vdwlem6  14062  0ram  14096  imasmnd2  15473  imasgrp2  15685  pmtrfrn  15979  pgpssslw  16128  efgsfo  16251  efgrelexlemb  16262  gexex  16350  imasrng  16726  mpfind  17637  mpfpf1  17800  pf1mpf  17801  lindfrn  18265  bwthOLD  19029  2ndcomap  19077  kgenidm  19135  kqreglem1  19329  zfbas  19484  rnelfmlem  19540  rnelfm  19541  fmfnfmlem2  19543  ovolctb  20988  ovolicc2  21020  mbfinf  21158  dvivth  21497  dvne0  21498  aannenlem3  21811  reeff1o  21927  usgraedgrn  23315  usgra2edg  23316  usgrarnedg  23318  rnbra  25526  cnvbraval  25529  pjssdif1i  25594  dfpjop  25601  elpjrn  25609  esumfsup  26534  ghomgrpilem2  27320  tailfb  28617  indexdom  28647  nacsfix  29067  fvelrnbf  29759  cncmpmax  29773  stoweidlem27  29841  stoweidlem31  29845  stoweidlem48  29862  stoweidlem59  29873  stirlinglem13  29900  vdn0frgrav2  30635  vdgn0frgrav2  30636  cdleme50rnlem  34207  diaelrnN  34709  diaintclN  34722  cdlemm10N  34782  dibintclN  34831  dihglb2  35006  dihintcl  35008  lcfrlem9  35214  mapd1o  35312  hdmaprnlem11N  35527  hgmaprnlem4N  35566
  Copyright terms: Public domain W3C validator