Theorem ffvelrn 6968

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Assertion

Ref	Expression
ffvelrn	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelrn

Step	Hyp	Ref	Expression
1		ffn 6609	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6967	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 580	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6616	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3921	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 481	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ran crn 5591   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445

This theorem is referenced by:  ffvelrni  6969  ffvelrnda  6970  dffo3  6987  foco2  6992  ffnfv  7001  ffvresb  7007  fcompt  7014  fsn2  7017  fvconst  7045  fprb  7078  f1cofveqaeq  7140  2f1fvneq  7142  fcofo  7169  cocan1  7172  isocnv  7210  isocnv3  7212  isores2  7213  isopolem  7225  isosolem  7227  fovrn  7451  off  7560  fnwelem  7981  smofvon2  8196  smorndom  8208  omsmolem  8496  omsmo  8497  fsetfcdm  8657  mapfvd  8676  mapsncnv  8690  2dom  8829  xpdom2  8863  domunsncan  8868  xpmapenlem  8940  fiint  9100  infdifsn  9424  cantnflem1  9456  wemapwe  9464  cnfcom3lem  9470  updjudhf  9698  fseqenlem1  9789  finacn  9815  ackbij1lem12  9996  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  coftr  10038  isf32lem6  10123  isf32lem7  10124  isf34lem7  10144  isf34lem6  10145  acncc  10205  axdc2lem  10213  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  ttukeylem6  10279  alephreg  10347  pwcfsdom  10348  canthp1lem2  10418  canthp1  10419  pwfseqlem1  10423  pwfseqlem4a  10426  gruf  10576  fsequb2  13705  axdc4uzlem  13712  seqf1o  13773  hashf1lem1  14177  hashf1lem1OLD  14178  wwlktovf  14680  shftf  14799  limsupgre  15199  rlimuni  15268  lo1resb  15282  o1resb  15284  o1of2  15331  o1rlimmul  15337  isercolllem1  15385  isercolllem2  15386  isercolllem3  15387  isercoll  15388  climsup  15390  iseralt  15405  sumeq2ii  15414  summolem2a  15436  isumcl  15482  isumshft  15560  climcndslem2  15571  climcnds  15572  mertenslem2  15606  prodeq2ii  15632  prodmolem2a  15653  iprodcl  15720  rpnnen2lem10  15941  ruclem8  15955  ruclem12  15959  3dvds  16049  smueqlem  16206  nn0seqcvgd  16284  algrf  16287  eucalg  16301  phimullem  16489  pcmpt  16602  pcprod  16605  vdwlem11  16701  vdwnnlem3  16707  ramlb  16729  0ram  16730  ramcl  16739  prmgaplem8  16768  imasaddfnlem  17248  imasaddflem  17250  mhmpropd  18445  smndex1gid  18551  ghmsub  18851  cntzmhm  18954  f1omvdconj  19063  pj1ghm  19318  gsumzaddlem  19531  gsumzadd  19532  gsummptnn0fzfv  19597  dprdfadd  19632  subgdmdprd  19646  gsumdixp  19857  lspcl  20247  znunit  20780  frlmsslsp  21012  frlmup2  21015  lindfmm  21043  islindf4  21054  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrbaglefi  21144  psrbaglefiOLD  21145  resspsrmul  21195  evlslem4  21293  evlslem3  21299  fvcoe1  21387  psropprmul  21418  00ply1bas  21420  subrgvr1cl  21442  coe1mul2lem1  21447  coe1tmmul  21457  ply1coe  21476  evl1val  21504  evl1sca  21509  pf1const  21521  1mavmul  21706  mavmulass  21707  marepvcl  21727  1marepvmarrepid  21733  cramerimplem1  21841  pmatcollpw3fi1lem1  21944  pmatcollpw3fi1lem2  21945  cpmadugsumlemF  22034  cpmadugsumfi  22035  cayleyhamilton1  22050  hauscmplem  22566  ptbasid  22735  ptpjcn  22771  upxp  22783  uptx  22785  txcmplem2  22802  xkopt  22815  txhmeo  22963  alexsubALTlem3  23209  nrginvrcn  23865  nmoi  23901  nmoleub  23904  cncfmet  24081  cnheibor  24127  evth  24131  pcopt  24194  pcopt2  24195  pcorevlem  24198  pi1xfrf  24225  pi1xfr  24227  pi1xfrcnvlem  24228  iscauf  24453  iscmet3lem1  24464  iscmet3lem2  24465  iscmet3  24466  causs  24471  bcthlem5  24501  bcth3  24504  ovolfcl  24639  ovolfioo  24640  ovolficc  24641  ovolficcss  24642  ovolfsval  24643  ovolmge0  24650  ovollb2lem  24661  ovolunlem1a  24669  ovoliunlem1  24675  ovoliunlem2  24676  ovoliun  24678  ovolicc1  24689  ovolicc2lem3  24692  ovolicc2lem4  24693  ovolicc2lem5  24694  voliunlem1  24723  volsup  24729  ioombl1lem2  24732  ovolfs2  24744  uniioovol  24752  uniiccvol  24753  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  uniioombllem6  24761  dyadmbl  24773  volcn  24779  ismbf  24801  mbfadd  24834  mbfsub  24835  mbflimsup  24839  0plef  24845  itg1climres  24888  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfmul  24900  xrge0f  24905  itg2ge0  24909  itg2seq  24916  itg2uba  24917  itg2lea  24918  itg2eqa  24919  itg2splitlem  24922  itg2split  24923  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  bddmulibl  25012  ellimc3  25052  dvaddbr  25111  dvcobr  25119  dvcj  25123  dvfre  25124  dvcnvlem  25149  dvlip  25166  dvlipcn  25167  c1lip1  25170  tdeglem4  25233  tdeglem4OLD  25234  tdeglem2  25235  coe1mul3  25273  ply1rem  25337  fta1g  25341  ig1pdvds  25350  plyf  25368  plyeq0lem  25380  plypf1  25382  plyaddlem  25385  plymullem  25386  plyco  25411  dgreq  25414  0dgrb  25416  coefv0  25418  coeaddlem  25419  coemullem  25420  coemulc  25425  plycn  25431  dgrcolem2  25444  plycjlem  25446  plycj  25447  plyrecj  25449  plyreres  25452  dvply1  25453  vieta1lem2  25480  vieta1  25481  elqaalem2  25489  aareccl  25495  aalioulem1  25501  ulmcaulem  25562  ulmcau  25563  ulmcn  25567  mtest  25572  psergf  25580  dvradcnv  25589  psercn2  25591  pserdvlem2  25596  pserdv2  25598  abelthlem6  25604  abelthlem8  25607  abelthlem9  25608  logtayl  25824  amgm  26149  ftalem1  26231  ftalem2  26232  ftalem3  26233  ftalem4  26234  ftalem5  26235  basellem2  26240  muinv  26351  dchrmulcl  26406  dchrinvcl  26410  dchrfi  26412  dchrghm  26413  dchrsum2  26425  dchrsum  26426  bposlem5  26445  lgscllem  26461  lgsval4a  26476  lgsneg  26478  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgseisenlem3  26534  rpvmasumlem  26644  dchrmusum2  26651  dchrvmasumiflem1  26658  dchrisum0ff  26664  dchrisum0flblem1  26665  dchrisum0fno1  26668  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem2a  26674  upgrreslem  27680  umgrreslem  27681  wlkpvtx  28036  wlkepvtx  28037  usgr2pthlem  28140  frgrncvvdeqlem8  28679  lnoadd  29129  lnosub  29130  nmosetre  29135  nmooge0  29138  nmoub3i  29144  nmounbi  29147  phoeqi  29228  ubthlem1  29241  h2hcau  29350  h2hlm  29351  hoscl  30116  homcl  30117  hodcl  30118  hoaddcl  30129  homulcl  30130  homulid2  30171  homco1  30172  homulass  30173  hoadddi  30174  hoadddir  30175  hoeq1  30201  hoeq2  30202  adjsym  30204  nmopsetretALT  30234  nmfnsetre  30248  cnvadj  30263  hhcno  30275  hhcnf  30276  nmopub2tALT  30280  nmopge0  30282  unopf1o  30287  unoplin  30291  counop  30292  nmfnleub2  30297  nmfnge0  30298  hmoplin  30313  eigvalcl  30332  lnop0  30337  hmops  30391  hmopm  30392  nlelchi  30432  leop2  30495  leopadd  30503  leopmuli  30504  leopnmid  30509  hmopidmchi  30522  pjinvari  30562  sticl  30586  fcomptf  31004  rge0scvg  31908  esumcst  32040  esumfzf  32046  esumfsup  32047  esumfsupre  32048  hasheuni  32062  measdivcstALTV  32202  eulerpartlems  32336  eulerpartlemgc  32338  eulerpartlemb  32344  derangsn  33141  subfacp1lem5  33155  subfacp1lem6  33156  pconnconn  33202  sconnpi1  33210  txsconnlem  33211  cvxsconn  33214  cvmliftphtlem  33288  cvmlift3lem2  33291  cvmlift3lem4  33293  cvmlift3lem6  33295  satfvel  33383  satefvfmla1  33396  elmrsubrn  33491  msubff  33501  msubvrs  33531  mclsssvlem  33533  faclim  33721  soseq  33812  curf  35764  uncf  35765  curunc  35768  unccur  35769  matunitlindflem1  35782  matunitlindflem2  35783  ptrecube  35786  heicant  35821  mblfinlem2  35824  itg2addnclem  35837  ftc1anclem1  35859  ftc1anclem2  35860  ftc1anclem4  35862  upixp  35896  fdc  35912  seqpo  35914  incsequz  35915  incsequz2  35916  metf1o  35922  geomcau  35926  sstotbnd2  35941  prdsbnd  35960  ismtyima  35970  ismtyhmeolem  35971  heiborlem3  35980  heiborlem6  35983  heiborlem10  35987  bfplem1  35989  ghomco  36058  sticksstones11  40119  mzpclall  40556  mzprename  40578  rexrabdioph  40623  rmydioph  40843  rmxdioph  40845  expdiophlem2  40851  expdioph  40852  pw2f1ocnv  40866  kelac1  40895  rngunsnply  41005  ofsubid  41949  ofdivrec  41951  ofdivcan4  41952  ofdivdiv2  41953  dvconstbi  41959  refsum2cnlem1  42587  dffo3f  42724  climinf  43154  stoweidlem26  43574  stoweidlem60  43608  stoweid  43611  dmvolsal  43892  caratheodory  44073  elhoi  44087  smfresal  44333  f1oresf1o2  44794  fargshiftf  44903  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  isomushgr  45289  isomgrtrlem  45301  mgmhmpropd  45350  rmsupp0  45715  domnmsuppn0  45716  gsumlsscl  45730  lincfsuppcl  45765  linccl  45766  lincdifsn  45776  lincsum  45781  lincscm  45782  lincscmcl  45784  lincext1  45806  lindslinindimp2lem1  45810  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  snlindsntor  45823  lincresunitlem2  45828  lincresunit3lem1  45831  lincresunit3lem2  45832  lincresunit3  45833  lincreslvec3  45834  isldepslvec2  45837  zlmodzxzldeplem3  45854  1arympt1  45995  ackendofnn0  46041  aacllem  46516