Theorem ffvelcdm 7084

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

Assertion

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

Proof of Theorem ffvelcdm

Step	Hyp	Ref	Expression
1		ffn 6718	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7083	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6725	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3982	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 482	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ran crn 5678   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  ffvelcdmi  7086  ffvelcdmda  7087  dffo3  7104  foco2  7109  ffnfv  7118  ffvresb  7124  fcompt  7131  fsn2  7134  fvconst  7162  fprb  7195  f1cofveqaeq  7257  2f1fvneq  7259  fcofo  7286  cocan1  7289  isocnv  7327  isocnv3  7329  isores2  7330  isopolem  7342  isosolem  7344  fovcdm  7577  off  7688  fnwelem  8117  soseq  8145  smofvon2  8356  smocdmdom  8368  omsmolem  8656  omsmo  8657  fsetfcdm  8854  mapfvd  8873  mapsncnv  8887  2dom  9030  xpdom2  9067  domunsncan  9072  xpmapenlem  9144  fiint  9324  infdifsn  9652  cantnflem1  9684  wemapwe  9692  cnfcom3lem  9698  updjudhf  9926  fseqenlem1  10019  finacn  10045  ackbij1lem12  10226  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  coftr  10268  isf32lem6  10353  isf32lem7  10354  isf34lem7  10374  isf34lem6  10375  acncc  10435  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  ttukeylem6  10509  alephreg  10577  pwcfsdom  10578  canthp1lem2  10648  canthp1  10649  pwfseqlem1  10653  pwfseqlem4a  10656  gruf  10806  fsequb2  13941  axdc4uzlem  13948  seqf1o  14009  hashf1lem1  14415  hashf1lem1OLD  14416  wwlktovf  14907  shftf  15026  limsupgre  15425  rlimuni  15494  lo1resb  15508  o1resb  15510  o1of2  15557  o1rlimmul  15563  isercolllem1  15611  isercolllem2  15612  isercolllem3  15613  isercoll  15614  climsup  15616  iseralt  15631  sumeq2ii  15639  summolem2a  15661  isumcl  15707  isumshft  15785  climcndslem2  15796  climcnds  15797  mertenslem2  15831  prodeq2ii  15857  prodmolem2a  15878  iprodcl  15945  rpnnen2lem10  16166  ruclem8  16180  ruclem12  16184  3dvds  16274  smueqlem  16431  nn0seqcvgd  16507  algrf  16510  eucalg  16524  phimullem  16712  pcmpt  16825  pcprod  16828  vdwlem11  16924  vdwnnlem3  16930  ramlb  16952  0ram  16953  ramcl  16962  prmgaplem8  16991  imasaddfnlem  17474  imasaddflem  17476  mhmpropd  18678  smndex1gid  18784  ghmsub  19100  cntzmhm  19205  f1omvdconj  19314  pj1ghm  19571  gsumzaddlem  19789  gsumzadd  19790  gsummptnn0fzfv  19855  dprdfadd  19890  subgdmdprd  19904  gsumdixp  20131  lspcl  20587  znunit  21119  frlmsslsp  21351  frlmup2  21354  lindfmm  21382  islindf4  21393  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbaglefi  21485  psrbaglefiOLD  21486  resspsrmul  21537  evlslem4  21637  evlslem3  21643  fvcoe1  21731  psropprmul  21760  00ply1bas  21762  subrgvr1cl  21784  coe1mul2lem1  21789  coe1tmmul  21799  ply1coe  21820  evl1val  21848  evl1sca  21853  pf1const  21865  1mavmul  22050  mavmulass  22051  marepvcl  22071  1marepvmarrepid  22077  cramerimplem1  22185  pmatcollpw3fi1lem1  22288  pmatcollpw3fi1lem2  22289  cpmadugsumlemF  22378  cpmadugsumfi  22379  cayleyhamilton1  22394  hauscmplem  22910  ptbasid  23079  ptpjcn  23115  upxp  23127  uptx  23129  txcmplem2  23146  xkopt  23159  txhmeo  23307  alexsubALTlem3  23553  nrginvrcn  24209  nmoi  24245  nmoleub  24248  cncfmet  24425  cnheibor  24471  evth  24475  pcopt  24538  pcopt2  24539  pcorevlem  24542  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  iscauf  24797  iscmet3lem1  24808  iscmet3lem2  24809  iscmet3  24810  causs  24815  bcthlem5  24845  bcth3  24848  ovolfcl  24983  ovolfioo  24984  ovolficc  24985  ovolficcss  24986  ovolfsval  24987  ovolmge0  24994  ovollb2lem  25005  ovolunlem1a  25013  ovoliunlem1  25019  ovoliunlem2  25020  ovoliun  25022  ovolicc1  25033  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2lem5  25038  voliunlem1  25067  volsup  25073  ioombl1lem2  25076  ovolfs2  25088  uniioovol  25096  uniiccvol  25097  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombllem6  25105  dyadmbl  25117  volcn  25123  ismbf  25145  mbfadd  25178  mbfsub  25179  mbflimsup  25183  0plef  25189  itg1climres  25232  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfmul  25244  xrge0f  25249  itg2ge0  25253  itg2seq  25260  itg2uba  25261  itg2lea  25262  itg2eqa  25263  itg2splitlem  25266  itg2split  25267  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  bddmulibl  25356  ellimc3  25396  dvaddbr  25455  dvcobr  25463  dvcj  25467  dvfre  25468  dvcnvlem  25493  dvlip  25510  dvlipcn  25511  c1lip1  25514  tdeglem4  25577  tdeglem4OLD  25578  tdeglem2  25579  coe1mul3  25617  ply1rem  25681  fta1g  25685  ig1pdvds  25694  plyf  25712  plyeq0lem  25724  plypf1  25726  plyaddlem  25729  plymullem  25730  plyco  25755  dgreq  25758  0dgrb  25760  coefv0  25762  coeaddlem  25763  coemullem  25764  coemulc  25769  plycn  25775  dgrcolem2  25788  plycjlem  25790  plycj  25791  plyrecj  25793  plyreres  25796  dvply1  25797  vieta1lem2  25824  vieta1  25825  elqaalem2  25833  aareccl  25839  aalioulem1  25845  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  mtest  25916  psergf  25924  dvradcnv  25933  psercn2  25935  pserdvlem2  25940  pserdv2  25942  abelthlem6  25948  abelthlem8  25951  abelthlem9  25952  logtayl  26168  amgm  26495  ftalem1  26577  ftalem2  26578  ftalem3  26579  ftalem4  26580  ftalem5  26581  basellem2  26586  muinv  26697  dchrmulcl  26752  dchrinvcl  26756  dchrfi  26758  dchrghm  26759  dchrsum2  26771  dchrsum  26772  bposlem5  26791  lgscllem  26807  lgsval4a  26822  lgsneg  26824  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  lgseisenlem3  26880  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumiflem1  27004  dchrisum0ff  27010  dchrisum0flblem1  27011  dchrisum0fno1  27014  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem2a  27020  upgrreslem  28561  umgrreslem  28562  wlkpvtx  28916  wlkepvtx  28917  usgr2pthlem  29020  frgrncvvdeqlem8  29559  lnoadd  30011  lnosub  30012  nmosetre  30017  nmooge0  30020  nmoub3i  30026  nmounbi  30029  phoeqi  30110  ubthlem1  30123  h2hcau  30232  h2hlm  30233  hoscl  30998  homcl  30999  hodcl  31000  hoaddcl  31011  homulcl  31012  homullid  31053  homco1  31054  homulass  31055  hoadddi  31056  hoadddir  31057  hoeq1  31083  hoeq2  31084  adjsym  31086  nmopsetretALT  31116  nmfnsetre  31130  cnvadj  31145  hhcno  31157  hhcnf  31158  nmopub2tALT  31162  nmopge0  31164  unopf1o  31169  unoplin  31173  counop  31174  nmfnleub2  31179  nmfnge0  31180  hmoplin  31195  eigvalcl  31214  lnop0  31219  hmops  31273  hmopm  31274  nlelchi  31314  leop2  31377  leopadd  31385  leopmuli  31386  leopnmid  31391  hmopidmchi  31404  pjinvari  31444  sticl  31468  fcomptf  31883  rge0scvg  32929  esumcst  33061  esumfzf  33067  esumfsup  33068  esumfsupre  33069  hasheuni  33083  measdivcstALTV  33223  eulerpartlems  33359  eulerpartlemgc  33361  eulerpartlemb  33367  derangsn  34161  subfacp1lem5  34175  subfacp1lem6  34176  pconnconn  34222  sconnpi1  34230  txsconnlem  34231  cvxsconn  34234  cvmliftphtlem  34308  cvmlift3lem2  34311  cvmlift3lem4  34313  cvmlift3lem6  34315  satfvel  34403  satefvfmla1  34416  elmrsubrn  34511  msubff  34521  msubvrs  34551  mclsssvlem  34553  faclim  34716  gg-dvcobr  35176  gg-plycn  35177  gg-psercn2  35178  curf  36466  uncf  36467  curunc  36470  unccur  36471  matunitlindflem1  36484  matunitlindflem2  36485  ptrecube  36488  heicant  36523  mblfinlem2  36526  itg2addnclem  36539  ftc1anclem1  36561  ftc1anclem2  36562  ftc1anclem4  36564  upixp  36597  fdc  36613  seqpo  36615  incsequz  36616  incsequz2  36617  metf1o  36623  geomcau  36627  sstotbnd2  36642  prdsbnd  36661  ismtyima  36671  ismtyhmeolem  36672  heiborlem3  36681  heiborlem6  36684  heiborlem10  36688  bfplem1  36690  ghomco  36759  sticksstones11  40972  mzpclall  41465  mzprename  41487  rexrabdioph  41532  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  pw2f1ocnv  41776  kelac1  41805  rngunsnply  41915  ofsubid  43083  ofdivrec  43085  ofdivcan4  43086  ofdivdiv2  43087  dvconstbi  43093  refsum2cnlem1  43721  dffo3f  43877  climinf  44322  stoweidlem26  44742  stoweidlem60  44776  stoweid  44779  dmvolsal  45062  caratheodory  45244  elhoi  45258  smfresal  45504  f1oresf1o2  45999  fargshiftf  46108  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  isomushgr  46494  isomgrtrlem  46506  mgmhmpropd  46555  rmsupp0  47044  domnmsuppn0  47045  gsumlsscl  47059  lincfsuppcl  47094  linccl  47095  lincdifsn  47105  lincsum  47110  lincscm  47111  lincscmcl  47113  lincext1  47135  lindslinindimp2lem1  47139  lindslinindimp2lem4  47142  lindslinindsimp2lem5  47143  snlindsntor  47152  lincresunitlem2  47157  lincresunit3lem1  47160  lincresunit3lem2  47161  lincresunit3  47162  lincreslvec3  47163  isldepslvec2  47166  zlmodzxzldeplem3  47183  1arympt1  47324  ackendofnn0  47370  aacllem  47848