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

Theorem ffvelrn 5868
Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
Assertion
Ref Expression
ffvelrn  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )

Proof of Theorem ffvelrn
StepHypRef Expression
1 ffn 5591 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5867 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 458 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5597 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3347 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 452 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
73, 6mpd 15 1  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   ran crn 4879    Fn wfn 5449   -->wf 5450   ` cfv 5454
This theorem is referenced by:  ffvelrni  5869  ffvelrnda  5870  dffo3  5884  foco2  5889  ffnfv  5894  ffvresb  5900  fcompt  5904  fsn2  5908  fvconst  5921  fcofo  6021  cocan1  6024  isocnv  6050  isocnv3  6052  isores2  6053  isopolem  6065  isosolem  6067  fovrn  6216  off  6320  fnwelem  6461  smofvon2  6618  smorndom  6630  omsmolem  6896  omsmo  6897  mapsncnv  7060  2dom  7179  xpdom2  7203  domunsncan  7208  xpmapenlem  7274  fiint  7383  ordiso2  7484  infdifsn  7611  cantnflem1  7645  wemapwe  7654  cnfcom3lem  7660  fseqenlem1  7905  finacn  7931  ackbij1lem12  8111  cofsmo  8149  cfsmolem  8150  cfcoflem  8152  coftr  8153  isf32lem6  8238  isf32lem7  8239  isf34lem7  8259  isf34lem6  8260  acncc  8320  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  axcclem  8337  ttukeylem6  8394  alephreg  8457  pwcfsdom  8458  canthp1lem2  8528  canthp1  8529  pwfseqlem1  8533  pwfseqlem4a  8536  gruf  8686  fsequb2  11315  axdc4uzlem  11321  seqf1o  11364  hashf1lem1  11704  eqs1  11761  shftf  11894  limsupgre  12275  rlimuni  12344  lo1resb  12358  o1resb  12360  o1of2  12406  o1rlimmul  12412  isercolllem1  12458  isercolllem2  12459  isercolllem3  12460  isercoll  12461  climsup  12463  iseralt  12478  sumeq2ii  12487  summolem2a  12509  isumcl  12545  isumshft  12619  climcndslem2  12630  climcnds  12631  mertenslem2  12662  rpnnen2lem10  12823  ruclem8  12836  ruclem12  12840  3dvds  12912  smueqlem  13002  nn0seqcvgd  13061  algrf  13064  eucalg  13078  phimullem  13168  pcmpt  13261  pcprod  13264  vdwlem11  13359  vdwnnlem3  13365  ramlb  13387  0ram  13388  ramcl  13397  imasaddfnlem  13753  imasaddflem  13755  mhmpropd  14744  ghmsub  15014  cntzmhm  15137  pj1ghm  15335  gsumzaddlem  15526  gsumzadd  15527  dprdfadd  15578  dprdf1o  15590  subgdmdprd  15592  gsumdixp  15715  lspcl  16052  psrbaglesupp  16433  psrbaglefi  16437  resspsrmul  16480  evlslem4  16564  fvcoe1  16605  psropprmul  16632  00ply1bas  16634  subrgvr1cl  16655  coe1mul2lem1  16660  coe1tmmul  16669  ply1coe  16684  znunit  16844  hauscmplem  17469  ptbasid  17607  ptpjcn  17643  upxp  17655  uptx  17657  txcmplem2  17674  xkopt  17687  txhmeo  17835  alexsubALTlem3  18080  nrginvrcn  18727  nmoi  18762  nmoleub  18765  cncfmet  18938  cnheibor  18980  evth  18984  pcopt  19047  pcopt2  19048  pcorevlem  19051  pi1xfrf  19078  pi1xfr  19080  pi1xfrcnvlem  19081  iscauf  19233  iscmet3lem1  19244  iscmet3lem2  19245  iscmet3  19246  causs  19251  bcthlem5  19281  bcth3  19284  ovolfcl  19363  ovolfioo  19364  ovolficc  19365  ovolficcss  19366  ovolfsval  19367  ovolmge0  19373  ovollb2lem  19384  ovolunlem1a  19392  ovoliunlem1  19398  ovoliunlem2  19399  ovoliun  19401  ovolicc1  19412  ovolicc2lem3  19415  ovolicc2lem4  19416  ovolicc2lem5  19417  voliunlem1  19444  volsup  19450  ioombl1lem2  19453  ovolfs2  19463  uniioovol  19471  uniiccvol  19472  uniioombllem3a  19476  uniioombllem3  19477  uniioombllem4  19478  uniioombllem5  19479  uniioombllem6  19480  dyadmbl  19492  volcn  19498  ismbf  19522  mbfadd  19553  mbfsub  19554  mbflimsup  19558  0plef  19564  itg1climres  19606  mbfi1fseqlem1  19607  mbfi1fseqlem3  19609  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfmul  19618  xrge0f  19623  itg2ge0  19627  itg2seq  19634  itg2uba  19635  itg2lea  19636  itg2eqa  19637  itg2splitlem  19640  itg2split  19641  itg2i1fseqle  19646  itg2i1fseq  19647  itg2i1fseq2  19648  itg2addlem  19650  bddmulibl  19730  ellimc3  19766  dvaddbr  19824  dvcobr  19832  dvcj  19836  dvfre  19837  dvcnvlem  19860  dvlip  19877  dvlipcn  19878  c1lip1  19881  evlslem3  19935  evl1val  19948  evl1sca  19950  pf1const  19966  tdeglem4  19983  tdeglem2  19984  coe1mul3  20022  ply1rem  20086  fta1g  20090  ig1pdvds  20099  plyf  20117  plyeq0lem  20129  plypf1  20131  plyaddlem  20134  plymullem  20135  plyco  20160  dgreq  20163  0dgrb  20165  coefv0  20166  coeaddlem  20167  coemullem  20168  coemulc  20173  plycn  20179  dgrcolem2  20192  plycjlem  20194  plycj  20195  plyrecj  20197  plyreres  20200  dvply1  20201  vieta1lem2  20228  vieta1  20229  elqaalem2  20237  aareccl  20243  aalioulem1  20249  ulmcaulem  20310  ulmcau  20311  ulmcn  20315  mtest  20320  psergf  20328  dvradcnv  20337  psercn2  20339  pserdvlem2  20344  pserdv2  20346  abelthlem6  20352  abelthlem8  20355  abelthlem9  20356  logtayl  20551  amgm  20829  ftalem1  20855  ftalem2  20856  ftalem3  20857  ftalem4  20858  ftalem5  20859  basellem2  20864  muinv  20978  dchrmulcl  21033  dchrinvcl  21037  dchrfi  21039  dchrghm  21040  dchrsum2  21052  dchrsum  21053  bposlem5  21072  lgscllem  21087  lgsval4a  21102  lgsneg  21103  lgsdir  21114  lgsdilem2  21115  lgsdi  21116  lgsne0  21117  lgseisenlem3  21135  rpvmasumlem  21181  dchrmusum2  21188  dchrvmasumiflem1  21195  dchrisum0ff  21201  dchrisum0flblem1  21202  dchrisum0fno1  21205  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lem2a  21211  usgrarnedg  21404  usgraedg4  21406  usgrares1  21424  usgrnloop  21563  cyclispthon  21620  fargshiftf  21623  usgrcyclnl2  21628  4cycl4dv  21654  vdgrnn0pnf  21680  ghgrplem2  21955  lnoadd  22259  lnosub  22260  nmosetre  22265  nmooge0  22268  nmoub3i  22274  nmounbi  22277  phoeqi  22359  ubthlem1  22372  h2hcau  22482  h2hlm  22483  hoscl  23248  homcl  23249  hodcl  23250  hoaddcl  23261  homulcl  23262  homulid2  23303  homco1  23304  homulass  23305  hoadddi  23306  hoadddir  23307  hoeq1  23333  hoeq2  23334  adjsym  23336  nmopsetretALT  23366  nmfnsetre  23380  cnvadj  23395  hhcno  23407  hhcnf  23408  nmopub2tALT  23412  nmopge0  23414  unopf1o  23419  unoplin  23423  counop  23424  nmfnleub2  23429  nmfnge0  23430  hmoplin  23445  eigvalcl  23464  lnop0  23469  hmops  23523  hmopm  23524  nlelchi  23564  leop2  23627  leopadd  23635  leopmuli  23636  leopnmid  23641  hmopidmchi  23654  pjinvari  23694  sticl  23718  fcomptf  24077  rge0scvg  24335  esumcst  24455  esumfzf  24459  esumfsup  24460  esumfsupre  24461  hasheuni  24475  measdivcstOLD  24578  derangsn  24856  subfacp1lem5  24870  subfacp1lem6  24871  pconcon  24918  sconpi1  24926  txsconlem  24927  cvxscon  24930  cvmliftphtlem  25004  cvmlift3lem2  25007  cvmlift3lem4  25009  cvmlift3lem6  25011  ghomgrpilem2  25097  ghomcl  25103  ghomgsg  25104  prodeq2ii  25239  prodmolem2a  25260  iprodcl  25314  faclim  25365  fprb  25397  soseq  25529  mblfinlem2  26244  itg2addnclem  26256  ftc1anclem1  26280  ftc1anclem2  26281  ftc1anclem4  26283  upixp  26431  fdc  26449  seqpo  26451  incsequz  26452  incsequz2  26453  metf1o  26461  geomcau  26465  sstotbnd2  26483  prdsbnd  26502  ismtyima  26512  ismtyhmeolem  26513  heiborlem3  26522  heiborlem6  26525  heiborlem10  26529  bfplem1  26531  ghomco  26558  mzpclall  26784  mzprename  26806  rexrabdioph  26854  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  expdioph  27094  pw2f1ocnv  27108  kelac1  27138  uvcresum  27219  frlmsslsp  27225  frlmup1  27227  frlmup2  27228  lindfmm  27274  islindf4  27285  rngunsnply  27355  f1omvdconj  27366  ofsubid  27518  ofdivrec  27520  ofdivcan4  27521  ofdivdiv2  27522  dvconstbi  27528  refsum2cnlem1  27684  climinf  27708  stoweidlem26  27751  stoweidlem60  27785  stoweid  27788  2f1fvneq  28077  cshw1v  28276  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  el2wlkonotlem  28329  usg2wlkonot  28350  usg2wotspth  28351  frgrancvvdeqlemB  28427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-fv 5462
  Copyright terms: Public domain W3C validator