Theorem ffvelrn 6902

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 6545	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6901	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 583	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6552	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3900	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 484	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  ran crn 5552   Fn wfn 6375  ⟶wf 6376  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fv 6388

This theorem is referenced by:  ffvelrni  6903  ffvelrnda  6904  dffo3  6921  foco2  6926  ffnfv  6935  ffvresb  6941  fcompt  6948  fsn2  6951  fvconst  6979  fprb  7009  f1cofveqaeq  7070  2f1fvneq  7072  fcofo  7098  cocan1  7101  isocnv  7139  isocnv3  7141  isores2  7142  isopolem  7154  isosolem  7156  fovrn  7378  off  7486  fnwelem  7898  smofvon2  8093  smorndom  8105  omsmolem  8382  omsmo  8383  fsetfcdm  8541  mapfvd  8560  mapsncnv  8574  2dom  8707  xpdom2  8740  domunsncan  8745  xpmapenlem  8813  fiint  8948  infdifsn  9272  cantnflem1  9304  wemapwe  9312  cnfcom3lem  9318  updjudhf  9547  fseqenlem1  9638  finacn  9664  ackbij1lem12  9845  cofsmo  9883  cfsmolem  9884  cfcoflem  9886  coftr  9887  isf32lem6  9972  isf32lem7  9973  isf34lem7  9993  isf34lem6  9994  acncc  10054  axdc2lem  10062  axdc3lem2  10065  axdc3lem4  10067  axdc4lem  10069  axcclem  10071  ttukeylem6  10128  alephreg  10196  pwcfsdom  10197  canthp1lem2  10267  canthp1  10268  pwfseqlem1  10272  pwfseqlem4a  10275  gruf  10425  fsequb2  13549  axdc4uzlem  13556  seqf1o  13617  hashf1lem1  14020  hashf1lem1OLD  14021  wwlktovf  14523  shftf  14642  limsupgre  15042  rlimuni  15111  lo1resb  15125  o1resb  15127  o1of2  15174  o1rlimmul  15180  isercolllem1  15228  isercolllem2  15229  isercolllem3  15230  isercoll  15231  climsup  15233  iseralt  15248  sumeq2ii  15257  summolem2a  15279  isumcl  15325  isumshft  15403  climcndslem2  15414  climcnds  15415  mertenslem2  15449  prodeq2ii  15475  prodmolem2a  15496  iprodcl  15563  rpnnen2lem10  15784  ruclem8  15798  ruclem12  15802  3dvds  15892  smueqlem  16049  nn0seqcvgd  16127  algrf  16130  eucalg  16144  phimullem  16332  pcmpt  16445  pcprod  16448  vdwlem11  16544  vdwnnlem3  16550  ramlb  16572  0ram  16573  ramcl  16582  prmgaplem8  16611  imasaddfnlem  17033  imasaddflem  17035  mhmpropd  18224  smndex1gid  18330  ghmsub  18630  cntzmhm  18733  f1omvdconj  18838  pj1ghm  19093  gsumzaddlem  19306  gsumzadd  19307  gsummptnn0fzfv  19372  dprdfadd  19407  subgdmdprd  19421  gsumdixp  19627  lspcl  20013  znunit  20528  frlmsslsp  20758  frlmup2  20761  lindfmm  20789  islindf4  20800  psrbaglesupp  20883  psrbaglesuppOLD  20884  psrbaglefi  20891  psrbaglefiOLD  20892  resspsrmul  20942  evlslem4  21034  evlslem3  21040  fvcoe1  21128  psropprmul  21159  00ply1bas  21161  subrgvr1cl  21183  coe1mul2lem1  21188  coe1tmmul  21198  ply1coe  21217  evl1val  21245  evl1sca  21250  pf1const  21262  1mavmul  21445  mavmulass  21446  marepvcl  21466  1marepvmarrepid  21472  cramerimplem1  21580  pmatcollpw3fi1lem1  21683  pmatcollpw3fi1lem2  21684  cpmadugsumlemF  21773  cpmadugsumfi  21774  cayleyhamilton1  21789  hauscmplem  22303  ptbasid  22472  ptpjcn  22508  upxp  22520  uptx  22522  txcmplem2  22539  xkopt  22552  txhmeo  22700  alexsubALTlem3  22946  nrginvrcn  23590  nmoi  23626  nmoleub  23629  cncfmet  23806  cnheibor  23852  evth  23856  pcopt  23919  pcopt2  23920  pcorevlem  23923  pi1xfrf  23950  pi1xfr  23952  pi1xfrcnvlem  23953  iscauf  24177  iscmet3lem1  24188  iscmet3lem2  24189  iscmet3  24190  causs  24195  bcthlem5  24225  bcth3  24228  ovolfcl  24363  ovolfioo  24364  ovolficc  24365  ovolficcss  24366  ovolfsval  24367  ovolmge0  24374  ovollb2lem  24385  ovolunlem1a  24393  ovoliunlem1  24399  ovoliunlem2  24400  ovoliun  24402  ovolicc1  24413  ovolicc2lem3  24416  ovolicc2lem4  24417  ovolicc2lem5  24418  voliunlem1  24447  volsup  24453  ioombl1lem2  24456  ovolfs2  24468  uniioovol  24476  uniiccvol  24477  uniioombllem3a  24481  uniioombllem3  24482  uniioombllem4  24483  uniioombllem5  24484  uniioombllem6  24485  dyadmbl  24497  volcn  24503  ismbf  24525  mbfadd  24558  mbfsub  24559  mbflimsup  24563  0plef  24569  itg1climres  24612  mbfi1fseqlem1  24613  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  mbfi1fseqlem5  24617  mbfmul  24624  xrge0f  24629  itg2ge0  24633  itg2seq  24640  itg2uba  24641  itg2lea  24642  itg2eqa  24643  itg2splitlem  24646  itg2split  24647  itg2i1fseqle  24652  itg2i1fseq  24653  itg2i1fseq2  24654  itg2addlem  24656  bddmulibl  24736  ellimc3  24776  dvaddbr  24835  dvcobr  24843  dvcj  24847  dvfre  24848  dvcnvlem  24873  dvlip  24890  dvlipcn  24891  c1lip1  24894  tdeglem4  24957  tdeglem4OLD  24958  tdeglem2  24959  coe1mul3  24997  ply1rem  25061  fta1g  25065  ig1pdvds  25074  plyf  25092  plyeq0lem  25104  plypf1  25106  plyaddlem  25109  plymullem  25110  plyco  25135  dgreq  25138  0dgrb  25140  coefv0  25142  coeaddlem  25143  coemullem  25144  coemulc  25149  plycn  25155  dgrcolem2  25168  plycjlem  25170  plycj  25171  plyrecj  25173  plyreres  25176  dvply1  25177  vieta1lem2  25204  vieta1  25205  elqaalem2  25213  aareccl  25219  aalioulem1  25225  ulmcaulem  25286  ulmcau  25287  ulmcn  25291  mtest  25296  psergf  25304  dvradcnv  25313  psercn2  25315  pserdvlem2  25320  pserdv2  25322  abelthlem6  25328  abelthlem8  25331  abelthlem9  25332  logtayl  25548  amgm  25873  ftalem1  25955  ftalem2  25956  ftalem3  25957  ftalem4  25958  ftalem5  25959  basellem2  25964  muinv  26075  dchrmulcl  26130  dchrinvcl  26134  dchrfi  26136  dchrghm  26137  dchrsum2  26149  dchrsum  26150  bposlem5  26169  lgscllem  26185  lgsval4a  26200  lgsneg  26202  lgsdir  26213  lgsdilem2  26214  lgsdi  26215  lgsne0  26216  lgseisenlem3  26258  rpvmasumlem  26368  dchrmusum2  26375  dchrvmasumiflem1  26382  dchrisum0ff  26388  dchrisum0flblem1  26389  dchrisum0fno1  26392  rpvmasum2  26393  dchrisum0re  26394  dchrisum0lem2a  26398  upgrreslem  27392  umgrreslem  27393  wlkpvtx  27747  wlkepvtx  27748  usgr2pthlem  27850  frgrncvvdeqlem8  28389  lnoadd  28839  lnosub  28840  nmosetre  28845  nmooge0  28848  nmoub3i  28854  nmounbi  28857  phoeqi  28938  ubthlem1  28951  h2hcau  29060  h2hlm  29061  hoscl  29826  homcl  29827  hodcl  29828  hoaddcl  29839  homulcl  29840  homulid2  29881  homco1  29882  homulass  29883  hoadddi  29884  hoadddir  29885  hoeq1  29911  hoeq2  29912  adjsym  29914  nmopsetretALT  29944  nmfnsetre  29958  cnvadj  29973  hhcno  29985  hhcnf  29986  nmopub2tALT  29990  nmopge0  29992  unopf1o  29997  unoplin  30001  counop  30002  nmfnleub2  30007  nmfnge0  30008  hmoplin  30023  eigvalcl  30042  lnop0  30047  hmops  30101  hmopm  30102  nlelchi  30142  leop2  30205  leopadd  30213  leopmuli  30214  leopnmid  30219  hmopidmchi  30232  pjinvari  30272  sticl  30296  fcomptf  30715  rge0scvg  31613  esumcst  31743  esumfzf  31749  esumfsup  31750  esumfsupre  31751  hasheuni  31765  measdivcstALTV  31905  eulerpartlems  32039  eulerpartlemgc  32041  eulerpartlemb  32047  derangsn  32845  subfacp1lem5  32859  subfacp1lem6  32860  pconnconn  32906  sconnpi1  32914  txsconnlem  32915  cvxsconn  32918  cvmliftphtlem  32992  cvmlift3lem2  32995  cvmlift3lem4  32997  cvmlift3lem6  32999  satfvel  33087  satefvfmla1  33100  elmrsubrn  33195  msubff  33205  msubvrs  33235  mclsssvlem  33237  faclim  33430  soseq  33540  curf  35492  uncf  35493  curunc  35496  unccur  35497  matunitlindflem1  35510  matunitlindflem2  35511  ptrecube  35514  heicant  35549  mblfinlem2  35552  itg2addnclem  35565  ftc1anclem1  35587  ftc1anclem2  35588  ftc1anclem4  35590  upixp  35624  fdc  35640  seqpo  35642  incsequz  35643  incsequz2  35644  metf1o  35650  geomcau  35654  sstotbnd2  35669  prdsbnd  35688  ismtyima  35698  ismtyhmeolem  35699  heiborlem3  35708  heiborlem6  35711  heiborlem10  35715  bfplem1  35717  ghomco  35786  sticksstones11  39834  mzpclall  40252  mzprename  40274  rexrabdioph  40319  rmydioph  40539  rmxdioph  40541  expdiophlem2  40547  expdioph  40548  pw2f1ocnv  40562  kelac1  40591  rngunsnply  40701  ofsubid  41615  ofdivrec  41617  ofdivcan4  41618  ofdivdiv2  41619  dvconstbi  41625  refsum2cnlem1  42253  dffo3f  42390  climinf  42822  stoweidlem26  43242  stoweidlem60  43276  stoweid  43279  dmvolsal  43560  caratheodory  43741  elhoi  43755  smfresal  43994  f1oresf1o2  44455  fargshiftf  44565  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  isomushgr  44951  isomgrtrlem  44963  mgmhmpropd  45012  rmsupp0  45377  domnmsuppn0  45378  gsumlsscl  45392  lincfsuppcl  45427  linccl  45428  lincdifsn  45438  lincsum  45443  lincscm  45444  lincscmcl  45446  lincext1  45468  lindslinindimp2lem1  45472  lindslinindimp2lem4  45475  lindslinindsimp2lem5  45476  snlindsntor  45485  lincresunitlem2  45490  lincresunit3lem1  45493  lincresunit3lem2  45494  lincresunit3  45495  lincreslvec3  45496  isldepslvec2  45499  zlmodzxzldeplem3  45516  1arympt1  45657  ackendofnn0  45703  aacllem  46176