Theorem ffvelcdm 7081

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 6709	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7080	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6717	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3907	. . 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 2144  ran crn 5651   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  ffvelcdmi  7083  ffvelcdmda  7084  dffo3  7102  dffo3f  7106  foco2  7109  ffnfv  7119  ffvresb  7126  fcompt  7134  fsn2  7137  fvconst  7167  fprb  7199  f1cofveqaeq  7261  fcofo  7296  cocan1  7299  fvf1pr  7315  isocnv  7338  isocnv3  7340  isores2  7341  isopolem  7353  isosolem  7355  fovcdm  7591  off  7711  fnwelem  8143  soseq  8176  smofvon2  8364  smocdmdom  8376  omsmolem  8666  omsmo  8667  fsetfcdm  8882  curf  8890  uncf  8891  mapfvd  8907  mapsncnv  8921  2dom  9058  xpdom2  9091  domunsncan  9096  xpmapenlem  9163  fiint  9318  infdifsn  9658  cantnflem1  9690  wemapwe  9698  cnfcom3lem  9704  updjudhf  10012  fseqenlem1  10103  finacn  10129  ackbij1lem12  10308  cofsmo  10347  cfsmolem  10348  cfcoflem  10350  coftr  10351  isf32lem6  10436  isf32lem7  10437  isf34lem7  10457  isf34lem6  10458  acncc  10518  axdc2lem  10526  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  axcclem  10535  ttukeylem6  10592  alephreg  10667  pwcfsdom  10668  canthp1lem2  10738  canthp1  10739  pwfseqlem1  10743  pwfseqlem4a  10746  gruf  10896  fsequb2  14119  axdc4uzlem  14126  seqf1o  14186  hashf1lem1  14600  wwlktovf  15109  shftf  15232  limsupgre  15648  rlimuni  15717  lo1resb  15731  o1resb  15733  o1of2  15780  o1rlimmul  15786  isercolllem1  15832  isercolllem2  15833  isercolllem3  15834  isercoll  15835  climsup  15837  iseralt  15852  sumeq2ii  15860  summolem2a  15881  isumcl  15927  isumshft  16008  climcndslem2  16019  climcnds  16020  mertenslem2  16054  prodeq2ii  16080  prodmolem2a  16101  iprodcl  16168  rpnnen2lem10  16391  ruclem8  16405  ruclem12  16409  3dvds  16501  smueqlem  16660  nn0seqcvgd  16745  algrf  16748  eucalg  16762  phimullem  16956  pcmpt  17070  pcprod  17073  vdwlem11  17169  vdwnnlem3  17175  ramlb  17197  0ram  17198  ramcl  17207  prmgaplem8  17236  imasaddfnlem  17700  imasaddflem  17702  chnpof1  18804  mgmhmpropd  18887  mhmpropd  18987  smndex1gid  19100  smndex1gidOLD  19101  ghmsub  19438  cntzmhm  19555  f1omvdconj  19660  pj1ghm  19917  gsumzaddlem  20135  gsumzadd  20136  gsummptnn0fzfv  20201  dprdfadd  20236  subgdmdprd  20250  gsumdixp  20548  lspcl  21251  znunit  21869  frlmsslsp  22102  frlmup2  22105  lindfmm  22133  islindf4  22144  psrbaglesupp  22230  psrbaglefi  22234  resspsrmul  22283  evlslem4  22385  evlslem3  22389  fvcoe1  22525  psropprmul  22555  00ply1bas  22557  subrgvr1cl  22581  coe1mul2lem1  22586  coe1tmmul  22596  ply1coe  22616  evl1val  22647  evl1sca  22652  pf1const  22664  1mavmul  22863  mavmulass  22864  marepvcl  22884  1marepvmarrepid  22890  matunitlindflem1  22994  matunitlindflem2  22995  cramerimplem1  23001  pmatcollpw3fi1lem1  23104  pmatcollpw3fi1lem2  23105  cpmadugsumlemF  23194  cpmadugsumfi  23195  cayleyhamilton1  23210  hauscmplem  23724  ptbasid  23894  ptpjcn  23930  upxp  23942  uptx  23944  txcmplem2  23961  xkopt  23974  txhmeo  24122  alexsubALTlem3  24368  nrginvrcn  25011  nmoi  25047  nmoleub  25050  cncfmet  25230  cnheibor  25276  evth  25280  pcopt  25343  pcopt2  25344  pcorevlem  25347  pi1xfrf  25374  pi1xfr  25376  pi1xfrcnvlem  25377  iscauf  25601  iscmet3lem1  25612  iscmet3lem2  25613  iscmet3  25614  causs  25619  bcthlem5  25649  bcth3  25652  ovolfcl  25787  ovolfioo  25788  ovolficc  25789  ovolficcss  25790  ovolfsval  25791  ovolmge0  25798  ovollb2lem  25809  ovolunlem1a  25817  ovoliunlem1  25823  ovoliunlem2  25824  ovoliun  25826  ovolicc1  25837  ovolicc2lem3  25840  ovolicc2lem4  25841  ovolicc2lem5  25842  voliunlem1  25871  volsup  25877  ioombl1lem2  25880  ovolfs2  25892  uniioovol  25900  uniiccvol  25901  uniioombllem3a  25905  uniioombllem3  25906  uniioombllem4  25907  uniioombllem5  25908  uniioombllem6  25909  dyadmbl  25921  volcn  25927  ismbf  25949  mbfadd  25982  mbfsub  25983  mbflimsup  25987  0plef  25993  itg1climres  26035  mbfi1fseqlem1  26036  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  mbfmul  26047  xrge0f  26052  itg2ge0  26056  itg2seq  26063  itg2uba  26064  itg2lea  26065  itg2eqa  26066  itg2splitlem  26069  itg2split  26070  itg2i1fseqle  26075  itg2i1fseq  26076  itg2i1fseq2  26077  itg2addlem  26079  bddmulibl  26159  ellimc3  26199  dvaddbr  26258  dvcobr  26266  dvcj  26270  dvfre  26271  dvcnvlem  26296  dvlip  26313  dvlipcn  26314  c1lip1  26317  tdeglem4  26378  tdeglem2  26379  coe1mul3  26417  ply1rem  26484  fta1g  26488  ig1pdvds  26498  plyf  26516  plyeq0lem  26529  plypf1  26531  plyaddlem  26534  plymullem  26535  plyco  26560  dgreq  26563  0dgrb  26565  coefv0  26567  coeaddlem  26568  coemullem  26569  coemulc  26574  plycn  26580  dgrcolem2  26593  plycjlem  26595  plycj  26596  plyrecj  26598  plyreres  26604  dvply1  26605  vieta1lem2  26634  vieta1  26635  elqaalem2  26643  aareccl  26653  aalioulem1  26659  ulmcaulem  26721  ulmcau  26722  ulmcn  26726  mtest  26731  psergf  26739  dvradcnv  26748  psercn2  26750  pserdvlem2  26755  pserdv2  26757  abelthlem6  26763  abelthlem8  26766  abelthlem9  26767  logtayl  26988  amgm  27318  ftalem1  27400  ftalem2  27401  ftalem3  27402  ftalem4  27403  ftalem5  27404  basellem2  27409  muinv  27520  dchrmulcl  27576  dchrinvcl  27580  dchrfi  27582  dchrghm  27583  dchrsum2  27595  dchrsum  27596  bposlem5  27615  lgscllem  27631  lgsval4a  27646  lgsneg  27648  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  lgseisenlem3  27704  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasumiflem1  27828  dchrisum0ff  27834  dchrisum0flblem1  27835  dchrisum0fno1  27838  rpvmasum2  27839  dchrisum0re  27840  dchrisum0lem2a  27844  upgrreslem  29885  umgrreslem  29886  wlkpvtx  30238  wlkepvtx  30239  usgr2pthlem  30349  frgrncvvdeqlem8  30907  lnoadd  31360  lnosub  31361  nmosetre  31366  nmooge0  31369  nmoub3i  31375  nmounbi  31378  phoeqi  31459  ubthlem1  31472  h2hcau  31581  h2hlm  31582  hoscl  32347  homcl  32348  hodcl  32349  hoaddcl  32360  homulcl  32361  homullid  32402  homco1  32403  homulass  32404  hoadddi  32405  hoadddir  32406  hoeq1  32432  hoeq2  32433  adjsym  32435  nmopsetretALT  32465  nmfnsetre  32479  cnvadj  32494  hhcno  32506  hhcnf  32507  nmopub2tALT  32511  nmopge0  32513  unopf1o  32518  unoplin  32522  counop  32523  nmfnleub2  32528  nmfnge0  32529  hmoplin  32544  eigvalcl  32563  lnop0  32568  hmops  32622  hmopm  32623  nlelchi  32663  leop2  32726  leopadd  32734  leopmuli  32735  leopnmid  32740  hmopidmchi  32753  pjinvari  32793  sticl  32817  fcomptf  33252  rge0scvg  34581  esumcst  34695  esumfzf  34701  esumfsup  34702  esumfsupre  34703  hasheuni  34717  measdivcstALTV  34858  eulerpartlems  34992  eulerpartlemgc  34994  eulerpartlemb  35000  derangsn  35935  subfacp1lem5  35949  subfacp1lem6  35950  pconnconn  35996  sconnpi1  36004  txsconnlem  36005  cvxsconn  36008  cvmliftphtlem  36082  cvmlift3lem2  36085  cvmlift3lem4  36087  cvmlift3lem6  36089  satfvel  36177  satefvfmla1  36190  elmrsubrn  36285  msubff  36295  msubvrs  36325  mclsssvlem  36327  faclim  36511  curunc  38526  unccur  38527  ptrecube  38539  heicant  38574  mblfinlem2  38577  itg2addnclem  38590  ftc1anclem1  38612  ftc1anclem2  38613  ftc1anclem4  38615  upixp  38664  fdc  38680  seqpo  38682  incsequz  38683  incsequz2  38684  metf1o  38690  geomcau  38694  sstotbnd2  38709  prdsbnd  38728  ismtyima  38738  ismtyhmeolem  38739  heiborlem3  38748  heiborlem6  38751  heiborlem10  38755  bfplem1  38757  ghomco  38826  sticksstones11  43207  mzpclall  43738  mzprename  43760  rexrabdioph  43801  rmydioph  44021  rmxdioph  44023  expdiophlem2  44029  expdioph  44030  pw2f1ocnv  44044  kelac1  44065  rngunsnply  44171  ofsubid  45308  ofdivrec  45310  ofdivcan4  45311  ofdivdiv2  45312  dvconstbi  45318  refsum2cnlem1  46054  climinf  46618  stoweidlem26  47036  stoweidlem60  47070  stoweid  47073  dmvolsal  47356  caratheodory  47538  elhoi  47552  smfresal  47798  sqrtrrnpoly  47942  f1oresf1o2  48361  fargshiftf  48522  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  isubgrvtxuhgr  48962  isubgruhgr  48966  isubgr0uhgr  48971  grimuhgr  48985  gricushgr  49015  rmsupp0  49480  domnmsuppn0  49481  gsumlsscl  49492  lincfsuppcl  49525  linccl  49526  lincdifsn  49536  lincsum  49541  lincscm  49542  lincscmcl  49544  lincext1  49566  lindslinindimp2lem1  49570  lindslinindimp2lem4  49573  lindslinindsimp2lem5  49574  snlindsntor  49583  lincresunitlem2  49588  lincresunit3lem1  49591  lincresunit3lem2  49592  lincresunit3  49593  lincreslvec3  49594  isldepslvec2  49597  zlmodzxzldeplem3  49614  1arympt1  49750  ackendofnn0  49796  xpco2  49967  aacllem  50939