Theorem ffvelrn 6672

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Assertion

Ref	Expression
ffvelrn	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelrn

Step	Hyp	Ref	Expression
1		ffn 6342	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6671	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 572	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6348	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3856	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 473	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  ran crn 5405   Fn wfn 6181  ⟶wf 6182  ‘cfv 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pr 5184

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194

This theorem is referenced by:  ffvelrni  6673  ffvelrnda  6674  dffo3  6689  foco2  6694  ffnfv  6703  ffvresb  6709  fcompt  6716  fsn2  6719  fvconst  6747  fprb  6781  f1cofveqaeq  6839  2f1fvneq  6841  fcofo  6867  cocan1  6870  isocnv  6904  isocnv3  6906  isores2  6907  isopolem  6919  isosolem  6921  fovrn  7132  off  7240  fnwelem  7627  smofvon2  7794  smorndom  7806  omsmolem  8076  omsmo  8077  mapfvd  8239  mapsncnv  8251  2dom  8375  xpdom2  8404  domunsncan  8409  xpmapenlem  8476  fiint  8586  infdifsn  8910  cantnflem1  8942  wemapwe  8950  cnfcom3lem  8956  updjudhf  9150  fseqenlem1  9240  finacn  9266  ackbij1lem12  9447  cofsmo  9485  cfsmolem  9486  cfcoflem  9488  coftr  9489  isf32lem6  9574  isf32lem7  9575  isf34lem7  9595  isf34lem6  9596  acncc  9656  axdc2lem  9664  axdc3lem2  9667  axdc3lem4  9669  axdc4lem  9671  axcclem  9673  ttukeylem6  9730  alephreg  9798  pwcfsdom  9799  canthp1lem2  9869  canthp1  9870  pwfseqlem1  9874  pwfseqlem4a  9877  gruf  10027  fsequb2  13156  axdc4uzlem  13163  seqf1o  13223  hashf1lem1  13620  wwlktovf  14175  shftf  14293  limsupgre  14693  rlimuni  14762  lo1resb  14776  o1resb  14778  o1of2  14824  o1rlimmul  14830  isercolllem1  14876  isercolllem2  14877  isercolllem3  14878  isercoll  14879  climsup  14881  iseralt  14896  sumeq2ii  14904  summolem2a  14926  isumcl  14970  isumshft  15048  climcndslem2  15059  climcnds  15060  mertenslem2  15095  prodeq2ii  15121  prodmolem2a  15142  iprodcl  15209  rpnnen2lem10  15430  ruclem8  15444  ruclem12  15448  3dvds  15534  smueqlem  15693  nn0seqcvgd  15764  algrf  15767  eucalg  15781  phimullem  15966  pcmpt  16078  pcprod  16081  vdwlem11  16177  vdwnnlem3  16183  ramlb  16205  0ram  16206  ramcl  16215  prmgaplem8  16244  imasaddfnlem  16651  imasaddflem  16653  mhmpropd  17803  ghmsub  18131  cntzmhm  18234  f1omvdconj  18329  pj1ghm  18581  gsumzaddlem  18788  gsumzadd  18789  gsummptnn0fzfv  18851  dprdfadd  18886  subgdmdprd  18900  gsumdixp  19076  lspcl  19464  psrbaglesupp  19856  psrbaglefi  19860  resspsrmul  19905  evlslem4  19995  evlslem3  20001  fvcoe1  20072  psropprmul  20103  00ply1bas  20105  subrgvr1cl  20127  coe1mul2lem1  20132  coe1tmmul  20142  ply1coe  20161  evl1val  20188  evl1sca  20193  pf1const  20205  znunit  20406  frlmsslsp  20636  frlmup2  20639  lindfmm  20667  islindf4  20678  1mavmul  20855  mavmulass  20856  marepvcl  20876  1marepvmarrepid  20882  cramerimplem1  20990  pmatcollpw3fi1lem1  21092  pmatcollpw3fi1lem2  21093  cpmadugsumlemF  21182  cpmadugsumfi  21183  cayleyhamilton1  21198  hauscmplem  21712  ptbasid  21881  ptpjcn  21917  upxp  21929  uptx  21931  txcmplem2  21948  xkopt  21961  txhmeo  22109  alexsubALTlem3  22355  nrginvrcn  22998  nmoi  23034  nmoleub  23037  cncfmet  23213  cnheibor  23256  evth  23260  pcopt  23323  pcopt2  23324  pcorevlem  23327  pi1xfrf  23354  pi1xfr  23356  pi1xfrcnvlem  23357  iscauf  23580  iscmet3lem1  23591  iscmet3lem2  23592  iscmet3  23593  causs  23598  bcthlem5  23628  bcth3  23631  ovolfcl  23764  ovolfioo  23765  ovolficc  23766  ovolficcss  23767  ovolfsval  23768  ovolmge0  23775  ovollb2lem  23786  ovolunlem1a  23794  ovoliunlem1  23800  ovoliunlem2  23801  ovoliun  23803  ovolicc1  23814  ovolicc2lem3  23817  ovolicc2lem4  23818  ovolicc2lem5  23819  voliunlem1  23848  volsup  23854  ioombl1lem2  23857  ovolfs2  23869  uniioovol  23877  uniiccvol  23878  uniioombllem3a  23882  uniioombllem3  23883  uniioombllem4  23884  uniioombllem5  23885  uniioombllem6  23886  dyadmbl  23898  volcn  23904  ismbf  23926  mbfadd  23959  mbfsub  23960  mbflimsup  23964  0plef  23970  itg1climres  24012  mbfi1fseqlem1  24013  mbfi1fseqlem3  24015  mbfi1fseqlem4  24016  mbfi1fseqlem5  24017  mbfmul  24024  xrge0f  24029  itg2ge0  24033  itg2seq  24040  itg2uba  24041  itg2lea  24042  itg2eqa  24043  itg2splitlem  24046  itg2split  24047  itg2i1fseqle  24052  itg2i1fseq  24053  itg2i1fseq2  24054  itg2addlem  24056  bddmulibl  24136  ellimc3  24174  dvaddbr  24232  dvcobr  24240  dvcj  24244  dvfre  24245  dvcnvlem  24270  dvlip  24287  dvlipcn  24288  c1lip1  24291  tdeglem4  24351  tdeglem2  24352  coe1mul3  24390  ply1rem  24454  fta1g  24458  ig1pdvds  24467  plyf  24485  plyeq0lem  24497  plypf1  24499  plyaddlem  24502  plymullem  24503  plyco  24528  dgreq  24531  0dgrb  24533  coefv0  24535  coeaddlem  24536  coemullem  24537  coemulc  24542  plycn  24548  dgrcolem2  24561  plycjlem  24563  plycj  24564  plyrecj  24566  plyreres  24569  dvply1  24570  vieta1lem2  24597  vieta1  24598  elqaalem2  24606  aareccl  24612  aalioulem1  24618  ulmcaulem  24679  ulmcau  24680  ulmcn  24684  mtest  24689  psergf  24697  dvradcnv  24706  psercn2  24708  pserdvlem2  24713  pserdv2  24715  abelthlem6  24721  abelthlem8  24724  abelthlem9  24725  logtayl  24938  amgm  25264  ftalem1  25346  ftalem2  25347  ftalem3  25348  ftalem4  25349  ftalem5  25350  basellem2  25355  muinv  25466  dchrmulcl  25521  dchrinvcl  25525  dchrfi  25527  dchrghm  25528  dchrsum2  25540  dchrsum  25541  bposlem5  25560  lgscllem  25576  lgsval4a  25591  lgsneg  25593  lgsdir  25604  lgsdilem2  25605  lgsdi  25606  lgsne0  25607  lgseisenlem3  25649  rpvmasumlem  25759  dchrmusum2  25766  dchrvmasumiflem1  25773  dchrisum0ff  25779  dchrisum0flblem1  25780  dchrisum0fno1  25783  rpvmasum2  25784  dchrisum0re  25785  dchrisum0lem2a  25789  upgrreslem  26783  umgrreslem  26784  wlkpvtx  27137  wlkepvtx  27138  wlkresOLD  27152  usgr2pthlem  27246  frgrncvvdeqlem8  27834  lnoadd  28306  lnosub  28307  nmosetre  28312  nmooge0  28315  nmoub3i  28321  nmounbi  28324  phoeqi  28406  ubthlem1  28419  h2hcau  28529  h2hlm  28530  hoscl  29297  homcl  29298  hodcl  29299  hoaddcl  29310  homulcl  29311  homulid2  29352  homco1  29353  homulass  29354  hoadddi  29355  hoadddir  29356  hoeq1  29382  hoeq2  29383  adjsym  29385  nmopsetretALT  29415  nmfnsetre  29429  cnvadj  29444  hhcno  29456  hhcnf  29457  nmopub2tALT  29461  nmopge0  29463  unopf1o  29468  unoplin  29472  counop  29473  nmfnleub2  29478  nmfnge0  29479  hmoplin  29494  eigvalcl  29513  lnop0  29518  hmops  29572  hmopm  29573  nlelchi  29613  leop2  29676  leopadd  29684  leopmuli  29685  leopnmid  29690  hmopidmchi  29703  pjinvari  29743  sticl  29767  fcomptf  30159  rge0scvg  30827  esumcst  30957  esumfzf  30963  esumfsup  30964  esumfsupre  30965  hasheuni  30979  measdivcstOLD  31119  eulerpartlems  31254  eulerpartlemgc  31256  eulerpartlemb  31262  derangsn  31992  subfacp1lem5  32006  subfacp1lem6  32007  pconnconn  32053  sconnpi1  32061  txsconnlem  32062  cvxsconn  32065  cvmliftphtlem  32139  cvmlift3lem2  32142  cvmlift3lem4  32144  cvmlift3lem6  32146  elmrsubrn  32257  msubff  32267  msubvrs  32297  mclsssvlem  32299  faclim  32468  soseq  32587  curf  34289  uncf  34290  curunc  34293  unccur  34294  matunitlindflem1  34307  matunitlindflem2  34308  ptrecube  34311  heicant  34346  mblfinlem2  34349  itg2addnclem  34362  ftc1anclem1  34386  ftc1anclem2  34387  ftc1anclem4  34389  upixp  34424  fdc  34440  seqpo  34442  incsequz  34443  incsequz2  34444  metf1o  34450  geomcau  34454  sstotbnd2  34472  prdsbnd  34491  ismtyima  34501  ismtyhmeolem  34502  heiborlem3  34511  heiborlem6  34514  heiborlem10  34518  bfplem1  34520  ghomco  34589  mzpclall  38697  mzprename  38719  rexrabdioph  38765  rmydioph  38985  rmxdioph  38987  expdiophlem2  38993  expdioph  38994  pw2f1ocnv  39008  kelac1  39037  rngunsnply  39147  ofsubid  40049  ofdivrec  40051  ofdivcan4  40052  ofdivdiv2  40053  dvconstbi  40059  refsum2cnlem1  40690  dffo3f  40841  climinf  41297  stoweidlem26  41721  stoweidlem60  41755  stoweid  41758  dmvolsal  42039  caratheodory  42220  elhoi  42234  smfresal  42473  f1oresf1o2  42875  fargshiftf  42951  nnsum4primeseven  43307  nnsum4primesevenALTV  43308  isomushgr  43333  isomgrtrlem  43345  mgmhmpropd  43394  rmsupp0  43756  domnmsuppn0  43757  gsumlsscl  43771  lincfsuppcl  43809  linccl  43810  lincdifsn  43820  lincsum  43825  lincscm  43826  lincscmcl  43828  lincext1  43850  lindslinindimp2lem1  43854  lindslinindimp2lem4  43857  lindslinindsimp2lem5  43858  snlindsntor  43867  lincresunitlem2  43872  lincresunit3lem1  43875  lincresunit3lem2  43876  lincresunit3  43877  lincreslvec3  43878  isldepslvec2  43881  zlmodzxzldeplem3  43898  aacllem  44243