Theorem ffvelcdm 7102

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 6728	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7101	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6736	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3912	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 16	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ran crn 5656   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563

This theorem is used by:  ffvelcdmi  7104  ffvelcdmda  7105  dffo3  7123  dffo3f  7127  foco2  7130  ffnfv  7140  ffvresb  7147  fcompt  7155  fsn2  7158  fvconst  7188  fprb  7219  f1cofveqaeq  7281  fcofo  7316  cocan1  7319  fvf1pr  7335  isocnv  7358  isocnv3  7360  isores2  7361  isopolem  7373  isosolem  7375  fovcdm  7612  off  7732  fnwelem  8167  soseq  8200  smofvon2  8389  smocdmdom  8401  omsmolem  8691  omsmo  8692  fsetfcdm  8907  curf  8915  uncf  8916  mapfvd  8932  mapsncnv  8946  2dom  9083  xpdom2  9116  domunsncan  9121  xpmapenlem  9188  fiint  9343  infdifsn  9682  cantnflem1  9714  wemapwe  9722  cnfcom3lem  9728  updjudhf  10036  fseqenlem1  10127  finacn  10153  ackbij1lem12  10332  cofsmo  10371  cfsmolem  10372  cfcoflem  10374  coftr  10375  isf32lem6  10460  isf32lem7  10461  isf34lem7  10481  isf34lem6  10482  acncc  10542  axdc2lem  10550  axdc3lem2  10553  axdc3lem4  10555  axdc4lem  10557  axcclem  10559  ttukeylem6  10616  alephreg  10691  pwcfsdom  10692  canthp1lem2  10762  canthp1  10763  pwfseqlem1  10767  pwfseqlem4a  10770  gruf  10920  fsequb2  14143  axdc4uzlem  14150  seqf1o  14210  hashf1lem1  14624  wwlktovf  15135  shftf  15258  limsupgre  15674  rlimuni  15743  lo1resb  15757  o1resb  15759  o1of2  15806  o1rlimmul  15812  isercolllem1  15858  isercolllem2  15859  isercolllem3  15860  isercoll  15861  climsup  15863  iseralt  15878  sumeq2ii  15886  summolem2a  15907  isumcl  15953  isumshft  16034  climcndslem2  16045  climcnds  16046  mertenslem2  16080  prodeq2ii  16106  prodmolem2a  16127  iprodcl  16194  rpnnen2lem10  16417  ruclem8  16431  ruclem12  16435  3dvds  16527  smueqlem  16686  nn0seqcvgd  16771  algrf  16774  eucalg  16788  phimullem  16982  pcmpt  17096  pcprod  17099  vdwlem11  17195  vdwnnlem3  17201  ramlb  17223  0ram  17224  ramcl  17233  prmgaplem8  17262  imasaddfnlem  17726  imasaddflem  17728  chnpof1  18830  mgmhmpropd  18913  mhmpropd  19013  smndex1gid  19126  smndex1gidOLD  19127  ghmsub  19464  cntzmhm  19582  f1omvdconj  19687  pj1ghm  19944  gsumzaddlem  20162  gsumzadd  20163  gsummptnn0fzfv  20228  dprdfadd  20263  subgdmdprd  20277  gsumdixp  20575  lspcl  21278  znunit  21896  frlmsslsp  22129  frlmup2  22132  lindfmm  22160  islindf4  22171  psrbaglesupp  22257  psrbaglefi  22261  resspsrmul  22310  evlslem4  22412  evlslem3  22416  fvcoe1  22552  psropprmul  22582  00ply1bas  22584  subrgvr1cl  22608  coe1mul2lem1  22613  coe1tmmul  22623  ply1coe  22643  evl1val  22674  evl1sca  22679  pf1const  22691  1mavmul  22890  mavmulass  22891  marepvcl  22911  1marepvmarrepid  22917  matunitlindflem1  23021  matunitlindflem2  23022  cramerimplem1  23028  pmatcollpw3fi1lem1  23131  pmatcollpw3fi1lem2  23132  cpmadugsumlemF  23221  cpmadugsumfi  23222  cayleyhamilton1  23237  hauscmplem  23751  ptbasid  23921  ptpjcn  23957  upxp  23969  uptx  23971  txcmplem2  23988  xkopt  24001  txhmeo  24149  alexsubALTlem3  24395  nrginvrcn  25038  nmoi  25074  nmoleub  25077  cncfmet  25257  cnheibor  25303  evth  25307  pcopt  25370  pcopt2  25371  pcorevlem  25374  pi1xfrf  25401  pi1xfr  25403  pi1xfrcnvlem  25404  iscauf  25628  iscmet3lem1  25639  iscmet3lem2  25640  iscmet3  25641  causs  25646  bcthlem5  25676  bcth3  25679  ovolfcl  25814  ovolfioo  25815  ovolficc  25816  ovolficcss  25817  ovolfsval  25818  ovolmge0  25825  ovollb2lem  25836  ovolunlem1a  25844  ovoliunlem1  25850  ovoliunlem2  25851  ovoliun  25853  ovolicc1  25864  ovolicc2lem3  25867  ovolicc2lem4  25868  ovolicc2lem5  25869  voliunlem1  25898  volsup  25904  ioombl1lem2  25907  ovolfs2  25919  uniioovol  25927  uniiccvol  25928  uniioombllem3a  25932  uniioombllem3  25933  uniioombllem4  25934  uniioombllem5  25935  uniioombllem6  25936  dyadmbl  25948  volcn  25954  ismbf  25976  mbfadd  26009  mbfsub  26010  mbflimsup  26014  0plef  26020  itg1climres  26062  mbfi1fseqlem1  26063  mbfi1fseqlem3  26065  mbfi1fseqlem4  26066  mbfi1fseqlem5  26067  mbfmul  26074  xrge0f  26079  itg2ge0  26083  itg2seq  26090  itg2uba  26091  itg2lea  26092  itg2eqa  26093  itg2splitlem  26096  itg2split  26097  itg2i1fseqle  26102  itg2i1fseq  26103  itg2i1fseq2  26104  itg2addlem  26106  bddmulibl  26186  ellimc3  26226  dvaddbr  26285  dvcobr  26293  dvcj  26297  dvfre  26298  dvcnvlem  26323  dvlip  26340  dvlipcn  26341  c1lip1  26344  tdeglem4  26405  tdeglem2  26406  coe1mul3  26444  ply1rem  26511  fta1g  26515  ig1pdvds  26525  plyf  26543  plyeq0lem  26556  plypf1  26558  plyaddlem  26561  plymullem  26562  plyco  26587  dgreq  26590  0dgrb  26592  coefv0  26594  coeaddlem  26595  coemullem  26596  coemulc  26601  plycn  26607  dgrcolem2  26620  plycjlem  26622  plycj  26623  plyrecj  26625  plyreres  26631  dvply1  26632  vieta1lem2  26661  vieta1  26662  elqaalem2  26670  aareccl  26680  aalioulem1  26686  ulmcaulem  26748  ulmcau  26749  ulmcn  26753  mtest  26758  psergf  26766  dvradcnv  26775  psercn2  26777  pserdvlem2  26782  pserdv2  26784  abelthlem6  26790  abelthlem8  26793  abelthlem9  26794  logtayl  27015  amgm  27345  ftalem1  27427  ftalem2  27428  ftalem3  27429  ftalem4  27430  ftalem5  27431  basellem2  27436  muinv  27547  dchrmulcl  27603  dchrinvcl  27607  dchrfi  27609  dchrghm  27610  dchrsum2  27622  dchrsum  27623  bposlem5  27642  lgscllem  27658  lgsval4a  27673  lgsneg  27675  lgsdir  27686  lgsdilem2  27687  lgsdi  27688  lgsne0  27689  lgseisenlem3  27731  rpvmasumlem  27841  dchrmusum2  27848  dchrvmasumiflem1  27855  dchrisum0ff  27861  dchrisum0flblem1  27862  dchrisum0fno1  27865  rpvmasum2  27866  dchrisum0re  27867  dchrisum0lem2a  27871  upgrreslem  29912  umgrreslem  29913  wlkpvtx  30265  wlkepvtx  30266  usgr2pthlem  30376  frgrncvvdeqlem8  30934  lnoadd  31387  lnosub  31388  nmosetre  31393  nmooge0  31396  nmoub3i  31402  nmounbi  31405  phoeqi  31486  ubthlem1  31499  h2hcau  31608  h2hlm  31609  hoscl  32374  homcl  32375  hodcl  32376  hoaddcl  32387  homulcl  32388  homullid  32429  homco1  32430  homulass  32431  hoadddi  32432  hoadddir  32433  hoeq1  32459  hoeq2  32460  adjsym  32462  nmopsetretALT  32492  nmfnsetre  32506  cnvadj  32521  hhcno  32533  hhcnf  32534  nmopub2tALT  32538  nmopge0  32540  unopf1o  32545  unoplin  32549  counop  32550  nmfnleub2  32555  nmfnge0  32556  hmoplin  32571  eigvalcl  32590  lnop0  32595  hmops  32649  hmopm  32650  nlelchi  32690  leop2  32753  leopadd  32761  leopmuli  32762  leopnmid  32767  hmopidmchi  32780  pjinvari  32820  sticl  32844  fcomptf  33321  rge0scvg  34648  esumcst  34762  esumfzf  34768  esumfsup  34769  esumfsupre  34770  hasheuni  34784  measdivcstALTV  34925  eulerpartlems  35059  eulerpartlemgc  35061  eulerpartlemb  35067  derangsn  36101  subfacp1lem5  36115  subfacp1lem6  36116  pconnconn  36162  sconnpi1  36170  txsconnlem  36171  cvxsconn  36174  cvmliftphtlem  36248  cvmlift3lem2  36251  cvmlift3lem4  36253  cvmlift3lem6  36255  satfvel  36343  satefvfmla1  36356  elmrsubrn  36451  msubff  36461  msubvrs  36491  mclsssvlem  36493  faclim  36688  curunc  38716  unccur  38717  ptrecube  38729  heicant  38764  mblfinlem2  38767  itg2addnclem  38780  ftc1anclem1  38802  ftc1anclem2  38803  ftc1anclem4  38805  upixp  38854  fdc  38870  seqpo  38872  incsequz  38873  incsequz2  38874  metf1o  38880  geomcau  38884  sstotbnd2  38899  prdsbnd  38918  ismtyima  38928  ismtyhmeolem  38929  heiborlem3  38938  heiborlem6  38941  heiborlem10  38945  bfplem1  38947  ghomco  39016  sticksstones11  43397  mzpclall  43929  mzprename  43951  rexrabdioph  43992  rmydioph  44212  rmxdioph  44214  expdiophlem2  44220  expdioph  44221  pw2f1ocnv  44235  kelac1  44256  rngunsnply  44361  ofsubid  45498  ofdivrec  45500  ofdivcan4  45501  ofdivdiv2  45502  dvconstbi  45508  refsum2cnlem1  46257  climinf  46821  stoweidlem26  47239  stoweidlem60  47273  stoweid  47276  dmvolsal  47559  caratheodory  47741  elhoi  47755  smfresal  48001  sqrtrrnpoly  48145  f1oresf1o2  48564  fargshiftf  48725  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  isubgrvtxuhgr  49165  isubgruhgr  49169  isubgr0uhgr  49174  grimuhgr  49188  gricushgr  49218  rmsupp0  49683  domnmsuppn0  49684  gsumlsscl  49695  lincfsuppcl  49728  linccl  49729  lincdifsn  49739  lincsum  49744  lincscm  49745  lincscmcl  49747  lincext1  49769  lindslinindimp2lem1  49773  lindslinindimp2lem4  49776  lindslinindsimp2lem5  49777  snlindsntor  49786  lincresunitlem2  49791  lincresunit3lem1  49794  lincresunit3lem2  49795  lincresunit3  49796  lincreslvec3  49797  isldepslvec2  49800  zlmodzxzldeplem3  49817  1arympt1  49953  ackendofnn0  49999  xpco2  50171  aacllem  51217