Theorem ffvelcdm 7026

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 6662	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7025	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 580	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6669	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3932	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ran crn 5625   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  ffvelcdmi  7028  ffvelcdmda  7029  dffo3  7047  dffo3f  7051  foco2  7054  ffnfv  7064  ffvresb  7070  fcompt  7078  fsn2  7081  fvconst  7108  fprb  7140  f1cofveqaeq  7203  fcofo  7234  cocan1  7237  fvf1pr  7253  isocnv  7276  isocnv3  7278  isores2  7279  isopolem  7291  isosolem  7293  fovcdm  7528  off  7640  fnwelem  8073  soseq  8101  smofvon2  8288  smocdmdom  8300  omsmolem  8585  omsmo  8586  fsetfcdm  8797  mapfvd  8817  mapsncnv  8831  2dom  8967  xpdom2  9000  domunsncan  9005  xpmapenlem  9072  fiint  9227  infdifsn  9566  cantnflem1  9598  wemapwe  9606  cnfcom3lem  9612  updjudhf  9843  fseqenlem1  9934  finacn  9960  ackbij1lem12  10140  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  coftr  10183  isf32lem6  10268  isf32lem7  10269  isf34lem7  10289  isf34lem6  10290  acncc  10350  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  ttukeylem6  10424  alephreg  10493  pwcfsdom  10494  canthp1lem2  10564  canthp1  10565  pwfseqlem1  10569  pwfseqlem4a  10572  gruf  10722  fsequb2  13899  axdc4uzlem  13906  seqf1o  13966  hashf1lem1  14378  wwlktovf  14879  shftf  15002  limsupgre  15404  rlimuni  15473  lo1resb  15487  o1resb  15489  o1of2  15536  o1rlimmul  15542  isercolllem1  15588  isercolllem2  15589  isercolllem3  15590  isercoll  15591  climsup  15593  iseralt  15608  sumeq2ii  15616  summolem2a  15638  isumcl  15684  isumshft  15762  climcndslem2  15773  climcnds  15774  mertenslem2  15808  prodeq2ii  15834  prodmolem2a  15857  iprodcl  15924  rpnnen2lem10  16148  ruclem8  16162  ruclem12  16166  3dvds  16258  smueqlem  16417  nn0seqcvgd  16497  algrf  16500  eucalg  16514  phimullem  16706  pcmpt  16820  pcprod  16823  vdwlem11  16919  vdwnnlem3  16925  ramlb  16947  0ram  16948  ramcl  16957  prmgaplem8  16986  imasaddfnlem  17449  imasaddflem  17451  chnpof1  18553  mgmhmpropd  18623  mhmpropd  18717  smndex1gid  18828  ghmsub  19153  cntzmhm  19270  f1omvdconj  19375  pj1ghm  19632  gsumzaddlem  19850  gsumzadd  19851  gsummptnn0fzfv  19916  dprdfadd  19951  subgdmdprd  19965  gsumdixp  20254  lspcl  20927  znunit  21518  frlmsslsp  21751  frlmup2  21754  lindfmm  21782  islindf4  21793  psrbaglesupp  21878  psrbaglefi  21882  resspsrmul  21931  evlslem4  22031  evlslem3  22035  fvcoe1  22148  psropprmul  22178  00ply1bas  22180  subrgvr1cl  22204  coe1mul2lem1  22209  coe1tmmul  22219  ply1coe  22242  evl1val  22273  evl1sca  22278  pf1const  22290  1mavmul  22492  mavmulass  22493  marepvcl  22513  1marepvmarrepid  22519  cramerimplem1  22627  pmatcollpw3fi1lem1  22730  pmatcollpw3fi1lem2  22731  cpmadugsumlemF  22820  cpmadugsumfi  22821  cayleyhamilton1  22836  hauscmplem  23350  ptbasid  23519  ptpjcn  23555  upxp  23567  uptx  23569  txcmplem2  23586  xkopt  23599  txhmeo  23747  alexsubALTlem3  23993  nrginvrcn  24636  nmoi  24672  nmoleub  24675  cncfmet  24858  cnheibor  24910  evth  24914  pcopt  24978  pcopt2  24979  pcorevlem  24982  pi1xfrf  25009  pi1xfr  25011  pi1xfrcnvlem  25012  iscauf  25236  iscmet3lem1  25247  iscmet3lem2  25248  iscmet3  25249  causs  25254  bcthlem5  25284  bcth3  25287  ovolfcl  25423  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovolfsval  25427  ovolmge0  25434  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliunlem2  25460  ovoliun  25462  ovolicc1  25473  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2lem5  25478  voliunlem1  25507  volsup  25513  ioombl1lem2  25516  ovolfs2  25528  uniioovol  25536  uniiccvol  25537  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  dyadmbl  25557  volcn  25563  ismbf  25585  mbfadd  25618  mbfsub  25619  mbflimsup  25623  0plef  25629  itg1climres  25671  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfmul  25683  xrge0f  25688  itg2ge0  25692  itg2seq  25699  itg2uba  25700  itg2lea  25701  itg2eqa  25702  itg2splitlem  25705  itg2split  25706  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  bddmulibl  25796  ellimc3  25836  dvaddbr  25896  dvcobr  25905  dvcobrOLD  25906  dvcj  25910  dvfre  25911  dvcnvlem  25936  dvlip  25954  dvlipcn  25955  c1lip1  25958  tdeglem4  26021  tdeglem2  26022  coe1mul3  26060  ply1rem  26127  fta1g  26131  ig1pdvds  26141  plyf  26159  plyeq0lem  26171  plypf1  26173  plyaddlem  26176  plymullem  26177  plyco  26202  dgreq  26205  0dgrb  26207  coefv0  26209  coeaddlem  26210  coemullem  26211  coemulc  26216  plycn  26222  plycnOLD  26223  dgrcolem2  26236  plycjlem  26238  plycj  26239  plycjOLD  26241  plyrecj  26243  plyreres  26246  dvply1  26247  vieta1lem2  26275  vieta1  26276  elqaalem2  26284  aareccl  26290  aalioulem1  26296  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  mtest  26369  psergf  26377  dvradcnv  26386  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv2  26396  abelthlem6  26402  abelthlem8  26405  abelthlem9  26406  logtayl  26625  amgm  26957  ftalem1  27039  ftalem2  27040  ftalem3  27041  ftalem4  27042  ftalem5  27043  basellem2  27048  muinv  27159  dchrmulcl  27216  dchrinvcl  27220  dchrfi  27222  dchrghm  27223  dchrsum2  27235  dchrsum  27236  bposlem5  27255  lgscllem  27271  lgsval4a  27286  lgsneg  27288  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  lgseisenlem3  27344  rpvmasumlem  27454  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrisum0ff  27474  dchrisum0flblem1  27475  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem2a  27484  upgrreslem  29377  umgrreslem  29378  wlkpvtx  29731  wlkepvtx  29732  usgr2pthlem  29836  frgrncvvdeqlem8  30381  lnoadd  30833  lnosub  30834  nmosetre  30839  nmooge0  30842  nmoub3i  30848  nmounbi  30851  phoeqi  30932  ubthlem1  30945  h2hcau  31054  h2hlm  31055  hoscl  31820  homcl  31821  hodcl  31822  hoaddcl  31833  homulcl  31834  homullid  31875  homco1  31876  homulass  31877  hoadddi  31878  hoadddir  31879  hoeq1  31905  hoeq2  31906  adjsym  31908  nmopsetretALT  31938  nmfnsetre  31952  cnvadj  31967  hhcno  31979  hhcnf  31980  nmopub2tALT  31984  nmopge0  31986  unopf1o  31991  unoplin  31995  counop  31996  nmfnleub2  32001  nmfnge0  32002  hmoplin  32017  eigvalcl  32036  lnop0  32041  hmops  32095  hmopm  32096  nlelchi  32136  leop2  32199  leopadd  32207  leopmuli  32208  leopnmid  32213  hmopidmchi  32226  pjinvari  32266  sticl  32290  fcomptf  32736  rge0scvg  34106  esumcst  34220  esumfzf  34226  esumfsup  34227  esumfsupre  34228  hasheuni  34242  measdivcstALTV  34382  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemb  34525  derangsn  35364  subfacp1lem5  35378  subfacp1lem6  35379  pconnconn  35425  sconnpi1  35433  txsconnlem  35434  cvxsconn  35437  cvmliftphtlem  35511  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem6  35518  satfvel  35606  satefvfmla1  35619  elmrsubrn  35714  msubff  35724  msubvrs  35754  mclsssvlem  35756  faclim  35940  curf  37795  uncf  37796  curunc  37799  unccur  37800  matunitlindflem1  37813  matunitlindflem2  37814  ptrecube  37817  heicant  37852  mblfinlem2  37855  itg2addnclem  37868  ftc1anclem1  37890  ftc1anclem2  37891  ftc1anclem4  37893  upixp  37926  fdc  37942  seqpo  37944  incsequz  37945  incsequz2  37946  metf1o  37952  geomcau  37956  sstotbnd2  37971  prdsbnd  37990  ismtyima  38000  ismtyhmeolem  38001  heiborlem3  38010  heiborlem6  38013  heiborlem10  38017  bfplem1  38019  ghomco  38088  sticksstones11  42406  mzpclall  42965  mzprename  42987  rexrabdioph  43032  rmydioph  43252  rmxdioph  43254  expdiophlem2  43260  expdioph  43261  pw2f1ocnv  43275  kelac1  43301  rngunsnply  43407  ofsubid  44561  ofdivrec  44563  ofdivcan4  44564  ofdivdiv2  44565  dvconstbi  44571  refsum2cnlem1  45278  climinf  45848  stoweidlem26  46266  stoweidlem60  46300  stoweid  46303  dmvolsal  46586  caratheodory  46768  elhoi  46782  smfresal  47028  f1oresf1o2  47533  fargshiftf  47682  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  isubgrvtxuhgr  48106  isubgruhgr  48110  isubgr0uhgr  48115  grimuhgr  48129  gricushgr  48159  rmsupp0  48610  domnmsuppn0  48611  gsumlsscl  48622  lincfsuppcl  48655  linccl  48656  lincdifsn  48666  lincsum  48671  lincscm  48672  lincscmcl  48674  lincext1  48696  lindslinindimp2lem1  48700  lindslinindimp2lem4  48703  lindslinindsimp2lem5  48704  snlindsntor  48713  lincresunitlem2  48718  lincresunit3lem1  48721  lincresunit3lem2  48722  lincresunit3  48723  lincreslvec3  48724  isldepslvec2  48727  zlmodzxzldeplem3  48744  1arympt1  48880  ackendofnn0  48926  xpco2  49098  aacllem  50042