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

Theorem fvelrnb 5905
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 5904 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21eleq2d 2513 . 2  |-  ( F  Fn  A  ->  ( B  e.  ran  F  <->  B  e.  { y  |  E. x  e.  A  y  =  ( F `  x ) } ) )
3 fvex 5866 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2515 . . . . 5  |-  ( ( F `  x )  =  B  ->  (
( F `  x
)  e.  _V  <->  B  e.  _V ) )
53, 4mpbii 211 . . . 4  |-  ( ( F `  x )  =  B  ->  B  e.  _V )
65rexlimivw 2932 . . 3  |-  ( E. x  e.  A  ( F `  x )  =  B  ->  B  e.  _V )
7 eqeq1 2447 . . . . 5  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  B  =  ( F `  x ) ) )
8 eqcom 2452 . . . . 5  |-  ( B  =  ( F `  x )  <->  ( F `  x )  =  B )
97, 8syl6bb 261 . . . 4  |-  ( y  =  B  ->  (
y  =  ( F `
 x )  <->  ( F `  x )  =  B ) )
109rexbidv 2954 . . 3  |-  ( y  =  B  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  ( F `  x )  =  B ) )
116, 10elab3 3239 . 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 1383    e. wcel 1804   {cab 2428   E.wrex 2794   _Vcvv 3095   ran crn 4990    Fn wfn 5573   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-iota 5541  df-fun 5580  df-fn 5581  df-fv 5586
This theorem is referenced by:  foelrni  5906  chfnrn  5983  rexrn  6018  ralrn  6019  elrnrexdmb  6021  ffnfv  6042  fconstfvOLD  6119  elunirn  6148  isoini  6219  canth  6239  reldm  6836  seqomlem2  7118  fipreima  7828  ordiso2  7943  inf0  8041  inf3lem6  8053  noinfep  8079  noinfepOLD  8080  cantnflem4  8114  cantnflem4OLD  8136  infenaleph  8475  isinfcard  8476  dfac5  8512  ackbij1  8621  sornom  8660  fin23lem16  8718  fin23lem21  8722  isf32lem2  8737  fin1a2lem5  8787  itunitc  8804  axdc3lem2  8834  zorn2lem4  8882  cfpwsdom  8962  peano2nn  10555  uzn0  11107  om2uzrani  12045  uzrdgfni  12051  uzin2  13159  unbenlem  14408  vdwlem6  14486  0ram  14520  imasmnd2  15936  imasgrp2  16164  pmtrfrn  16462  pgpssslw  16613  efgsfo  16736  efgrelexlemb  16747  gexex  16838  imasring  17247  mpfind  18184  mpfpf1  18366  pf1mpf  18367  lindfrn  18834  bwthOLD  19889  2ndcomap  19937  kgenidm  20026  kqreglem1  20220  zfbas  20375  rnelfmlem  20431  rnelfm  20432  fmfnfmlem2  20434  ovolctb  21879  ovolicc2  21911  mbfinf  22050  dvivth  22389  dvne0  22390  aannenlem3  22704  reeff1o  22820  usgraedgrn  24359  usgra2edg  24360  usgrarnedg  24362  vdn0frgrav2  25001  vdgn0frgrav2  25002  rnbra  27004  cnvbraval  27007  pjssdif1i  27072  dfpjop  27079  elpjrn  27087  foresf1o  27381  esumfsup  28054  msrid  28883  ghomgrpilem2  29004  tailfb  30171  indexdom  30201  nacsfix  30620  fvelrnbf  31347  cncmpmax  31361  stoweidlem27  31763  stoweidlem31  31767  stoweidlem48  31784  stoweidlem59  31795  stirlinglem13  31822  fourierdlem12  31855  fourierdlem41  31884  fourierdlem42  31885  fourierdlem46  31889  fourierdlem48  31891  fourierdlem49  31892  fourierdlem70  31913  fourierdlem71  31914  fourierdlem74  31917  fourierdlem75  31918  fourierdlem102  31945  fourierdlem103  31946  fourierdlem104  31947  fourierdlem114  31957  cdleme50rnlem  36145  diaelrnN  36647  diaintclN  36660  cdlemm10N  36720  dibintclN  36769  dihglb2  36944  dihintcl  36946  lcfrlem9  37152  mapd1o  37250  hdmaprnlem11N  37465  hgmaprnlem4N  37504
  Copyright terms: Public domain W3C validator