Theorem ffvelcdm 7052

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ran crn 5654   Fn wfn 6511  ⟶wf 6512  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5276  ax-nul 5283  ax-pr 5404

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3419  df-v 3461  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-opab 5188  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524

This theorem is referenced by:  ffvelcdmi  7054  ffvelcdmda  7055  dffo3  7072  foco2  7077  ffnfv  7086  ffvresb  7092  fcompt  7099  fsn2  7102  fvconst  7130  fprb  7163  f1cofveqaeq  7225  2f1fvneq  7227  fcofo  7254  cocan1  7257  isocnv  7295  isocnv3  7297  isores2  7298  isopolem  7310  isosolem  7312  fovcdm  7544  off  7655  fnwelem  8083  soseq  8111  smofvon2  8322  smocdmdom  8334  omsmolem  8623  omsmo  8624  fsetfcdm  8820  mapfvd  8839  mapsncnv  8853  2dom  8996  xpdom2  9033  domunsncan  9038  xpmapenlem  9110  fiint  9290  infdifsn  9617  cantnflem1  9649  wemapwe  9657  cnfcom3lem  9663  updjudhf  9891  fseqenlem1  9984  finacn  10010  ackbij1lem12  10191  cofsmo  10229  cfsmolem  10230  cfcoflem  10232  coftr  10233  isf32lem6  10318  isf32lem7  10319  isf34lem7  10339  isf34lem6  10340  acncc  10400  axdc2lem  10408  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  ttukeylem6  10474  alephreg  10542  pwcfsdom  10543  canthp1lem2  10613  canthp1  10614  pwfseqlem1  10618  pwfseqlem4a  10621  gruf  10771  fsequb2  13906  axdc4uzlem  13913  seqf1o  13974  hashf1lem1  14380  hashf1lem1OLD  14381  wwlktovf  14872  shftf  14991  limsupgre  15390  rlimuni  15459  lo1resb  15473  o1resb  15475  o1of2  15522  o1rlimmul  15528  isercolllem1  15576  isercolllem2  15577  isercolllem3  15578  isercoll  15579  climsup  15581  iseralt  15596  sumeq2ii  15604  summolem2a  15626  isumcl  15672  isumshft  15750  climcndslem2  15761  climcnds  15762  mertenslem2  15796  prodeq2ii  15822  prodmolem2a  15843  iprodcl  15910  rpnnen2lem10  16131  ruclem8  16145  ruclem12  16149  3dvds  16239  smueqlem  16396  nn0seqcvgd  16472  algrf  16475  eucalg  16489  phimullem  16677  pcmpt  16790  pcprod  16793  vdwlem11  16889  vdwnnlem3  16895  ramlb  16917  0ram  16918  ramcl  16927  prmgaplem8  16956  imasaddfnlem  17439  imasaddflem  17441  mhmpropd  18637  smndex1gid  18742  ghmsub  19045  cntzmhm  19148  f1omvdconj  19257  pj1ghm  19514  gsumzaddlem  19727  gsumzadd  19728  gsummptnn0fzfv  19793  dprdfadd  19828  subgdmdprd  19842  gsumdixp  20062  lspcl  20509  znunit  21022  frlmsslsp  21254  frlmup2  21257  lindfmm  21285  islindf4  21296  psrbaglesupp  21378  psrbaglesuppOLD  21379  psrbaglefi  21386  psrbaglefiOLD  21387  resspsrmul  21438  evlslem4  21536  evlslem3  21542  fvcoe1  21630  psropprmul  21661  00ply1bas  21663  subrgvr1cl  21685  coe1mul2lem1  21690  coe1tmmul  21700  ply1coe  21719  evl1val  21747  evl1sca  21752  pf1const  21764  1mavmul  21949  mavmulass  21950  marepvcl  21970  1marepvmarrepid  21976  cramerimplem1  22084  pmatcollpw3fi1lem1  22187  pmatcollpw3fi1lem2  22188  cpmadugsumlemF  22277  cpmadugsumfi  22278  cayleyhamilton1  22293  hauscmplem  22809  ptbasid  22978  ptpjcn  23014  upxp  23026  uptx  23028  txcmplem2  23045  xkopt  23058  txhmeo  23206  alexsubALTlem3  23452  nrginvrcn  24108  nmoi  24144  nmoleub  24147  cncfmet  24324  cnheibor  24370  evth  24374  pcopt  24437  pcopt2  24438  pcorevlem  24441  pi1xfrf  24468  pi1xfr  24470  pi1xfrcnvlem  24471  iscauf  24696  iscmet3lem1  24707  iscmet3lem2  24708  iscmet3  24709  causs  24714  bcthlem5  24744  bcth3  24747  ovolfcl  24882  ovolfioo  24883  ovolficc  24884  ovolficcss  24885  ovolfsval  24886  ovolmge0  24893  ovollb2lem  24904  ovolunlem1a  24912  ovoliunlem1  24918  ovoliunlem2  24919  ovoliun  24921  ovolicc1  24932  ovolicc2lem3  24935  ovolicc2lem4  24936  ovolicc2lem5  24937  voliunlem1  24966  volsup  24972  ioombl1lem2  24975  ovolfs2  24987  uniioovol  24995  uniiccvol  24996  uniioombllem3a  25000  uniioombllem3  25001  uniioombllem4  25002  uniioombllem5  25003  uniioombllem6  25004  dyadmbl  25016  volcn  25022  ismbf  25044  mbfadd  25077  mbfsub  25078  mbflimsup  25082  0plef  25088  itg1climres  25131  mbfi1fseqlem1  25132  mbfi1fseqlem3  25134  mbfi1fseqlem4  25135  mbfi1fseqlem5  25136  mbfmul  25143  xrge0f  25148  itg2ge0  25152  itg2seq  25159  itg2uba  25160  itg2lea  25161  itg2eqa  25162  itg2splitlem  25165  itg2split  25166  itg2i1fseqle  25171  itg2i1fseq  25172  itg2i1fseq2  25173  itg2addlem  25175  bddmulibl  25255  ellimc3  25295  dvaddbr  25354  dvcobr  25362  dvcj  25366  dvfre  25367  dvcnvlem  25392  dvlip  25409  dvlipcn  25410  c1lip1  25413  tdeglem4  25476  tdeglem4OLD  25477  tdeglem2  25478  coe1mul3  25516  ply1rem  25580  fta1g  25584  ig1pdvds  25593  plyf  25611  plyeq0lem  25623  plypf1  25625  plyaddlem  25628  plymullem  25629  plyco  25654  dgreq  25657  0dgrb  25659  coefv0  25661  coeaddlem  25662  coemullem  25663  coemulc  25668  plycn  25674  dgrcolem2  25687  plycjlem  25689  plycj  25690  plyrecj  25692  plyreres  25695  dvply1  25696  vieta1lem2  25723  vieta1  25724  elqaalem2  25732  aareccl  25738  aalioulem1  25744  ulmcaulem  25805  ulmcau  25806  ulmcn  25810  mtest  25815  psergf  25823  dvradcnv  25832  psercn2  25834  pserdvlem2  25839  pserdv2  25841  abelthlem6  25847  abelthlem8  25850  abelthlem9  25851  logtayl  26067  amgm  26392  ftalem1  26474  ftalem2  26475  ftalem3  26476  ftalem4  26477  ftalem5  26478  basellem2  26483  muinv  26594  dchrmulcl  26649  dchrinvcl  26653  dchrfi  26655  dchrghm  26656  dchrsum2  26668  dchrsum  26669  bposlem5  26688  lgscllem  26704  lgsval4a  26719  lgsneg  26721  lgsdir  26732  lgsdilem2  26733  lgsdi  26734  lgsne0  26735  lgseisenlem3  26777  rpvmasumlem  26887  dchrmusum2  26894  dchrvmasumiflem1  26901  dchrisum0ff  26907  dchrisum0flblem1  26908  dchrisum0fno1  26911  rpvmasum2  26912  dchrisum0re  26913  dchrisum0lem2a  26917  upgrreslem  28349  umgrreslem  28350  wlkpvtx  28704  wlkepvtx  28705  usgr2pthlem  28808  frgrncvvdeqlem8  29347  lnoadd  29797  lnosub  29798  nmosetre  29803  nmooge0  29806  nmoub3i  29812  nmounbi  29815  phoeqi  29896  ubthlem1  29909  h2hcau  30018  h2hlm  30019  hoscl  30784  homcl  30785  hodcl  30786  hoaddcl  30797  homulcl  30798  homullid  30839  homco1  30840  homulass  30841  hoadddi  30842  hoadddir  30843  hoeq1  30869  hoeq2  30870  adjsym  30872  nmopsetretALT  30902  nmfnsetre  30916  cnvadj  30931  hhcno  30943  hhcnf  30944  nmopub2tALT  30948  nmopge0  30950  unopf1o  30955  unoplin  30959  counop  30960  nmfnleub2  30965  nmfnge0  30966  hmoplin  30981  eigvalcl  31000  lnop0  31005  hmops  31059  hmopm  31060  nlelchi  31100  leop2  31163  leopadd  31171  leopmuli  31172  leopnmid  31177  hmopidmchi  31190  pjinvari  31230  sticl  31254  fcomptf  31675  rge0scvg  32653  esumcst  32785  esumfzf  32791  esumfsup  32792  esumfsupre  32793  hasheuni  32807  measdivcstALTV  32947  eulerpartlems  33083  eulerpartlemgc  33085  eulerpartlemb  33091  derangsn  33885  subfacp1lem5  33899  subfacp1lem6  33900  pconnconn  33946  sconnpi1  33954  txsconnlem  33955  cvxsconn  33958  cvmliftphtlem  34032  cvmlift3lem2  34035  cvmlift3lem4  34037  cvmlift3lem6  34039  satfvel  34127  satefvfmla1  34140  elmrsubrn  34235  msubff  34245  msubvrs  34275  mclsssvlem  34277  faclim  34439  curf  36163  uncf  36164  curunc  36167  unccur  36168  matunitlindflem1  36181  matunitlindflem2  36182  ptrecube  36185  heicant  36220  mblfinlem2  36223  itg2addnclem  36236  ftc1anclem1  36258  ftc1anclem2  36259  ftc1anclem4  36261  upixp  36295  fdc  36311  seqpo  36313  incsequz  36314  incsequz2  36315  metf1o  36321  geomcau  36325  sstotbnd2  36340  prdsbnd  36359  ismtyima  36369  ismtyhmeolem  36370  heiborlem3  36379  heiborlem6  36382  heiborlem10  36386  bfplem1  36388  ghomco  36457  sticksstones11  40670  mzpclall  41141  mzprename  41163  rexrabdioph  41208  rmydioph  41429  rmxdioph  41431  expdiophlem2  41437  expdioph  41438  pw2f1ocnv  41452  kelac1  41481  rngunsnply  41591  ofsubid  42759  ofdivrec  42761  ofdivcan4  42762  ofdivdiv2  42763  dvconstbi  42769  refsum2cnlem1  43397  dffo3f  43553  climinf  44000  stoweidlem26  44420  stoweidlem60  44454  stoweid  44457  dmvolsal  44740  caratheodory  44922  elhoi  44936  smfresal  45182  f1oresf1o2  45676  fargshiftf  45785  nnsum4primeseven  46145  nnsum4primesevenALTV  46146  isomushgr  46171  isomgrtrlem  46183  mgmhmpropd  46232  rmsupp0  46597  domnmsuppn0  46598  gsumlsscl  46612  lincfsuppcl  46647  linccl  46648  lincdifsn  46658  lincsum  46663  lincscm  46664  lincscmcl  46666  lincext1  46688  lindslinindimp2lem1  46692  lindslinindimp2lem4  46695  lindslinindsimp2lem5  46696  snlindsntor  46705  lincresunitlem2  46710  lincresunit3lem1  46713  lincresunit3lem2  46714  lincresunit3  46715  lincreslvec3  46716  isldepslvec2  46719  zlmodzxzldeplem3  46736  1arympt1  46877  ackendofnn0  46923  aacllem  47401