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

Theorem fvelrnb 5917
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 5916 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21eleq2d 2516 . 2  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) } ) )
3 fvex 5880 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2519 . . . . 5  |-  ( ( F `  x )  =  B  ->  (
( F `  x
)  e.  _V  <->  B  e.  _V ) )
53, 4mpbii 215 . . . 4  |-  ( ( F `  x )  =  B  ->  B  e.  _V )
65rexlimivw 2878 . . 3  |-  ( E. x  e.  A  ( F `  x )  =  B  ->  B  e.  _V )
7 eqeq1 2457 . . . . 5  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  B  =  ( F `  x ) ) )
8 eqcom 2460 . . . . 5  |-  ( B  =  ( F `  x )  <->  ( F `  x )  =  B )
97, 8syl6bb 265 . . . 4  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  ( F `  x )  =  B ) )
109rexbidv 2903 . . 3  |-  ( y  =  B  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  ( F `  x )  =  B ) )
116, 10elab3 3194 . 2  |-  ( B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) }  <->  E. x  e.  A  ( F `  x )  =  B )
122, 11syl6bb 265 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 188    = wceq 1446    e. wcel 1889   {cab 2439   E.wrex 2740   _Vcvv 3047   ran crn 4838    Fn wfn 5580   ` cfv 5585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-fv 5593
This theorem is referenced by:  foelrni  5918  chfnrn  5998  rexrn  6029  ralrn  6030  elrnrexdmb  6032  ffnfv  6054  fconstfvOLD  6132  elunirn  6161  isoini  6234  canth  6254  reldm  6849  seqomlem2  7173  fipreima  7885  ordiso2  8035  inf0  8131  inf3lem6  8143  noinfep  8170  cantnflem4  8202  infenaleph  8527  isinfcard  8528  dfac5  8564  ackbij1  8673  sornom  8712  fin23lem16  8770  fin23lem21  8774  isf32lem2  8789  fin1a2lem5  8839  itunitc  8856  axdc3lem2  8886  zorn2lem4  8934  cfpwsdom  9014  peano2nn  10628  uzn0  11181  om2uzrani  12173  uzrdgfni  12179  uzin2  13419  unbenlem  14864  vdwlem6  14948  0ram  14990  imasmnd2  16585  imasgrp2  16813  pmtrfrn  17111  pgpssslw  17278  efgsfo  17401  efgrelexlemb  17412  gexex  17503  imasring  17859  mpfind  18771  mpfpf1  18951  pf1mpf  18952  lindfrn  19391  2ndcomap  20485  kgenidm  20574  kqreglem1  20768  zfbas  20923  rnelfmlem  20979  rnelfm  20980  fmfnfmlem2  20982  ovolctb  22455  ovolicc2  22488  mbfinf  22633  mbfinfOLD  22634  dvivth  22974  dvne0  22975  aannenlem3  23298  reeff1o  23414  usgraedgrn  25120  usgra2edg  25121  usgrarnedg  25123  vdn0frgrav2  25763  vdgn0frgrav2  25764  rnbra  27772  cnvbraval  27775  pjssdif1i  27840  dfpjop  27847  elpjrn  27855  foresf1o  28151  esumfsup  28903  esumiun  28927  msrid  30195  ghomgrpilem2  30316  tailfb  31045  indexdom  32073  cdleme50rnlem  34123  diaelrnN  34625  diaintclN  34638  cdlemm10N  34698  dibintclN  34747  dihglb2  34922  dihintcl  34924  lcfrlem9  35130  mapd1o  35228  hdmaprnlem11N  35443  hgmaprnlem4N  35482  nacsfix  35566  fvelrnbf  37349  cncmpmax  37363  stoweidlem27  37897  stoweidlem31  37902  stoweidlem48  37919  stoweidlem59  37930  stirlinglem13  37958  fourierdlem12  37991  fourierdlem41  38021  fourierdlem42  38022  fourierdlem42OLD  38023  fourierdlem46  38026  fourierdlem48  38028  fourierdlem49  38029  fourierdlem70  38050  fourierdlem71  38051  fourierdlem74  38054  fourierdlem75  38055  fourierdlem102  38082  fourierdlem103  38083  fourierdlem104  38084  fourierdlem114  38094  sge0tsms  38232  sge0sup  38243  sge0le  38259  sge0isum  38279  nnfoctbdjlem  38303  meadjiunlem  38313  iccpartrn  38754  iccpartnel  38762  usgr2edg  39301  ushgredgedga  39316  ushgredgedgaloop  39318  1pthon2v-av  39750  2pthon3v-av  39766
  Copyright terms: Public domain W3C validator