Theorem ffvelcdm 7053

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5639   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  ffvelcdmi  7055  ffvelcdmda  7056  dffo3  7074  dffo3f  7078  foco2  7081  ffnfv  7091  ffvresb  7097  fcompt  7105  fsn2  7108  fvconst  7136  fprb  7168  f1cofveqaeq  7232  fcofo  7263  cocan1  7266  fvf1pr  7282  isocnv  7305  isocnv3  7307  isores2  7308  isopolem  7320  isosolem  7322  fovcdm  7559  off  7671  fnwelem  8110  soseq  8138  smofvon2  8325  smocdmdom  8337  omsmolem  8621  omsmo  8622  fsetfcdm  8833  mapfvd  8852  mapsncnv  8866  2dom  9001  xpdom2  9036  domunsncan  9041  xpmapenlem  9108  fiint  9277  fiintOLD  9278  infdifsn  9610  cantnflem1  9642  wemapwe  9650  cnfcom3lem  9656  updjudhf  9884  fseqenlem1  9977  finacn  10003  ackbij1lem12  10183  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  coftr  10226  isf32lem6  10311  isf32lem7  10312  isf34lem7  10332  isf34lem6  10333  acncc  10393  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  ttukeylem6  10467  alephreg  10535  pwcfsdom  10536  canthp1lem2  10606  canthp1  10607  pwfseqlem1  10611  pwfseqlem4a  10614  gruf  10764  fsequb2  13941  axdc4uzlem  13948  seqf1o  14008  hashf1lem1  14420  wwlktovf  14922  shftf  15045  limsupgre  15447  rlimuni  15516  lo1resb  15530  o1resb  15532  o1of2  15579  o1rlimmul  15585  isercolllem1  15631  isercolllem2  15632  isercolllem3  15633  isercoll  15634  climsup  15636  iseralt  15651  sumeq2ii  15659  summolem2a  15681  isumcl  15727  isumshft  15805  climcndslem2  15816  climcnds  15817  mertenslem2  15851  prodeq2ii  15877  prodmolem2a  15900  iprodcl  15967  rpnnen2lem10  16191  ruclem8  16205  ruclem12  16209  3dvds  16301  smueqlem  16460  nn0seqcvgd  16540  algrf  16543  eucalg  16557  phimullem  16749  pcmpt  16863  pcprod  16866  vdwlem11  16962  vdwnnlem3  16968  ramlb  16990  0ram  16991  ramcl  17000  prmgaplem8  17029  imasaddfnlem  17491  imasaddflem  17493  mgmhmpropd  18625  mhmpropd  18719  smndex1gid  18830  ghmsub  19156  cntzmhm  19273  f1omvdconj  19376  pj1ghm  19633  gsumzaddlem  19851  gsumzadd  19852  gsummptnn0fzfv  19917  dprdfadd  19952  subgdmdprd  19966  gsumdixp  20228  lspcl  20882  znunit  21473  frlmsslsp  21705  frlmup2  21708  lindfmm  21736  islindf4  21747  psrbaglesupp  21831  psrbaglefi  21835  resspsrmul  21885  evlslem4  21983  evlslem3  21987  fvcoe1  22092  psropprmul  22122  00ply1bas  22124  subrgvr1cl  22148  coe1mul2lem1  22153  coe1tmmul  22163  ply1coe  22185  evl1val  22216  evl1sca  22221  pf1const  22233  1mavmul  22435  mavmulass  22436  marepvcl  22456  1marepvmarrepid  22462  cramerimplem1  22570  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  cpmadugsumlemF  22763  cpmadugsumfi  22764  cayleyhamilton1  22779  hauscmplem  23293  ptbasid  23462  ptpjcn  23498  upxp  23510  uptx  23512  txcmplem2  23529  xkopt  23542  txhmeo  23690  alexsubALTlem3  23936  nrginvrcn  24580  nmoi  24616  nmoleub  24619  cncfmet  24802  cnheibor  24854  evth  24858  pcopt  24922  pcopt2  24923  pcorevlem  24926  pi1xfrf  24953  pi1xfr  24955  pi1xfrcnvlem  24956  iscauf  25180  iscmet3lem1  25191  iscmet3lem2  25192  iscmet3  25193  causs  25198  bcthlem5  25228  bcth3  25231  ovolfcl  25367  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovolfsval  25371  ovolmge0  25378  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun  25406  ovolicc1  25417  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  voliunlem1  25451  volsup  25457  ioombl1lem2  25460  ovolfs2  25472  uniioovol  25480  uniiccvol  25481  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  dyadmbl  25501  volcn  25507  ismbf  25529  mbfadd  25562  mbfsub  25563  mbflimsup  25567  0plef  25573  itg1climres  25615  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfmul  25627  xrge0f  25632  itg2ge0  25636  itg2seq  25643  itg2uba  25644  itg2lea  25645  itg2eqa  25646  itg2splitlem  25649  itg2split  25650  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  bddmulibl  25740  ellimc3  25780  dvaddbr  25840  dvcobr  25849  dvcobrOLD  25850  dvcj  25854  dvfre  25855  dvcnvlem  25880  dvlip  25898  dvlipcn  25899  c1lip1  25902  tdeglem4  25965  tdeglem2  25966  coe1mul3  26004  ply1rem  26071  fta1g  26075  ig1pdvds  26085  plyf  26103  plyeq0lem  26115  plypf1  26117  plyaddlem  26120  plymullem  26121  plyco  26146  dgreq  26149  0dgrb  26151  coefv0  26153  coeaddlem  26154  coemullem  26155  coemulc  26160  plycn  26166  plycnOLD  26167  dgrcolem2  26180  plycjlem  26182  plycj  26183  plycjOLD  26185  plyrecj  26187  plyreres  26190  dvply1  26191  vieta1lem2  26219  vieta1  26220  elqaalem2  26228  aareccl  26234  aalioulem1  26240  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  mtest  26313  psergf  26321  dvradcnv  26330  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv2  26340  abelthlem6  26346  abelthlem8  26349  abelthlem9  26350  logtayl  26569  amgm  26901  ftalem1  26983  ftalem2  26984  ftalem3  26985  ftalem4  26986  ftalem5  26987  basellem2  26992  muinv  27103  dchrmulcl  27160  dchrinvcl  27164  dchrfi  27166  dchrghm  27167  dchrsum2  27179  dchrsum  27180  bposlem5  27199  lgscllem  27215  lgsval4a  27230  lgsneg  27232  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgseisenlem3  27288  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumiflem1  27412  dchrisum0ff  27418  dchrisum0flblem1  27419  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem2a  27428  upgrreslem  29231  umgrreslem  29232  wlkpvtx  29587  wlkepvtx  29588  usgr2pthlem  29693  frgrncvvdeqlem8  30235  lnoadd  30687  lnosub  30688  nmosetre  30693  nmooge0  30696  nmoub3i  30702  nmounbi  30705  phoeqi  30786  ubthlem1  30799  h2hcau  30908  h2hlm  30909  hoscl  31674  homcl  31675  hodcl  31676  hoaddcl  31687  homulcl  31688  homullid  31729  homco1  31730  homulass  31731  hoadddi  31732  hoadddir  31733  hoeq1  31759  hoeq2  31760  adjsym  31762  nmopsetretALT  31792  nmfnsetre  31806  cnvadj  31821  hhcno  31833  hhcnf  31834  nmopub2tALT  31838  nmopge0  31840  unopf1o  31845  unoplin  31849  counop  31850  nmfnleub2  31855  nmfnge0  31856  hmoplin  31871  eigvalcl  31890  lnop0  31895  hmops  31949  hmopm  31950  nlelchi  31990  leop2  32053  leopadd  32061  leopmuli  32062  leopnmid  32067  hmopidmchi  32080  pjinvari  32120  sticl  32144  fcomptf  32582  rge0scvg  33939  esumcst  34053  esumfzf  34059  esumfsup  34060  esumfsupre  34061  hasheuni  34075  measdivcstALTV  34215  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  derangsn  35157  subfacp1lem5  35171  subfacp1lem6  35172  pconnconn  35218  sconnpi1  35226  txsconnlem  35227  cvxsconn  35230  cvmliftphtlem  35304  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem6  35311  satfvel  35399  satefvfmla1  35412  elmrsubrn  35507  msubff  35517  msubvrs  35547  mclsssvlem  35549  faclim  35733  curf  37592  uncf  37593  curunc  37596  unccur  37597  matunitlindflem1  37610  matunitlindflem2  37611  ptrecube  37614  heicant  37649  mblfinlem2  37652  itg2addnclem  37665  ftc1anclem1  37687  ftc1anclem2  37688  ftc1anclem4  37690  upixp  37723  fdc  37739  seqpo  37741  incsequz  37742  incsequz2  37743  metf1o  37749  geomcau  37753  sstotbnd2  37768  prdsbnd  37787  ismtyima  37797  ismtyhmeolem  37798  heiborlem3  37807  heiborlem6  37810  heiborlem10  37814  bfplem1  37816  ghomco  37885  sticksstones11  42144  mzpclall  42715  mzprename  42737  rexrabdioph  42782  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  pw2f1ocnv  43026  kelac1  43052  rngunsnply  43158  ofsubid  44313  ofdivrec  44315  ofdivcan4  44316  ofdivdiv2  44317  dvconstbi  44323  refsum2cnlem1  45031  climinf  45604  stoweidlem26  46024  stoweidlem60  46058  stoweid  46061  dmvolsal  46344  caratheodory  46526  elhoi  46540  smfresal  46786  f1oresf1o2  47292  fargshiftf  47441  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  isubgrvtxuhgr  47864  isubgruhgr  47868  isubgr0uhgr  47873  grimuhgr  47887  gricushgr  47917  rmsupp0  48356  domnmsuppn0  48357  gsumlsscl  48368  lincfsuppcl  48402  linccl  48403  lincdifsn  48413  lincsum  48418  lincscm  48419  lincscmcl  48421  lincext1  48443  lindslinindimp2lem1  48447  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  snlindsntor  48460  lincresunitlem2  48465  lincresunit3lem1  48468  lincresunit3lem2  48469  lincresunit3  48470  lincreslvec3  48471  isldepslvec2  48474  zlmodzxzldeplem3  48491  1arympt1  48627  ackendofnn0  48673  xpco2  48845  aacllem  49790