Theorem ffvelrn 6941

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 6584	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6940	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 579	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6591	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3916	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5581   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426

This theorem is referenced by:  ffvelrni  6942  ffvelrnda  6943  dffo3  6960  foco2  6965  ffnfv  6974  ffvresb  6980  fcompt  6987  fsn2  6990  fvconst  7018  fprb  7051  f1cofveqaeq  7112  2f1fvneq  7114  fcofo  7140  cocan1  7143  isocnv  7181  isocnv3  7183  isores2  7184  isopolem  7196  isosolem  7198  fovrn  7420  off  7529  fnwelem  7943  smofvon2  8158  smorndom  8170  omsmolem  8447  omsmo  8448  fsetfcdm  8606  mapfvd  8625  mapsncnv  8639  2dom  8774  xpdom2  8807  domunsncan  8812  xpmapenlem  8880  fiint  9021  infdifsn  9345  cantnflem1  9377  wemapwe  9385  cnfcom3lem  9391  updjudhf  9620  fseqenlem1  9711  finacn  9737  ackbij1lem12  9918  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  coftr  9960  isf32lem6  10045  isf32lem7  10046  isf34lem7  10066  isf34lem6  10067  acncc  10127  axdc2lem  10135  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  ttukeylem6  10201  alephreg  10269  pwcfsdom  10270  canthp1lem2  10340  canthp1  10341  pwfseqlem1  10345  pwfseqlem4a  10348  gruf  10498  fsequb2  13624  axdc4uzlem  13631  seqf1o  13692  hashf1lem1  14096  hashf1lem1OLD  14097  wwlktovf  14599  shftf  14718  limsupgre  15118  rlimuni  15187  lo1resb  15201  o1resb  15203  o1of2  15250  o1rlimmul  15256  isercolllem1  15304  isercolllem2  15305  isercolllem3  15306  isercoll  15307  climsup  15309  iseralt  15324  sumeq2ii  15333  summolem2a  15355  isumcl  15401  isumshft  15479  climcndslem2  15490  climcnds  15491  mertenslem2  15525  prodeq2ii  15551  prodmolem2a  15572  iprodcl  15639  rpnnen2lem10  15860  ruclem8  15874  ruclem12  15878  3dvds  15968  smueqlem  16125  nn0seqcvgd  16203  algrf  16206  eucalg  16220  phimullem  16408  pcmpt  16521  pcprod  16524  vdwlem11  16620  vdwnnlem3  16626  ramlb  16648  0ram  16649  ramcl  16658  prmgaplem8  16687  imasaddfnlem  17156  imasaddflem  17158  mhmpropd  18351  smndex1gid  18457  ghmsub  18757  cntzmhm  18860  f1omvdconj  18969  pj1ghm  19224  gsumzaddlem  19437  gsumzadd  19438  gsummptnn0fzfv  19503  dprdfadd  19538  subgdmdprd  19552  gsumdixp  19763  lspcl  20153  znunit  20683  frlmsslsp  20913  frlmup2  20916  lindfmm  20944  islindf4  20955  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbaglefi  21045  psrbaglefiOLD  21046  resspsrmul  21096  evlslem4  21194  evlslem3  21200  fvcoe1  21288  psropprmul  21319  00ply1bas  21321  subrgvr1cl  21343  coe1mul2lem1  21348  coe1tmmul  21358  ply1coe  21377  evl1val  21405  evl1sca  21410  pf1const  21422  1mavmul  21605  mavmulass  21606  marepvcl  21626  1marepvmarrepid  21632  cramerimplem1  21740  pmatcollpw3fi1lem1  21843  pmatcollpw3fi1lem2  21844  cpmadugsumlemF  21933  cpmadugsumfi  21934  cayleyhamilton1  21949  hauscmplem  22465  ptbasid  22634  ptpjcn  22670  upxp  22682  uptx  22684  txcmplem2  22701  xkopt  22714  txhmeo  22862  alexsubALTlem3  23108  nrginvrcn  23762  nmoi  23798  nmoleub  23801  cncfmet  23978  cnheibor  24024  evth  24028  pcopt  24091  pcopt2  24092  pcorevlem  24095  pi1xfrf  24122  pi1xfr  24124  pi1xfrcnvlem  24125  iscauf  24349  iscmet3lem1  24360  iscmet3lem2  24361  iscmet3  24362  causs  24367  bcthlem5  24397  bcth3  24400  ovolfcl  24535  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovolfsval  24539  ovolmge0  24546  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun  24574  ovolicc1  24585  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  voliunlem1  24619  volsup  24625  ioombl1lem2  24628  ovolfs2  24640  uniioovol  24648  uniiccvol  24649  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  dyadmbl  24669  volcn  24675  ismbf  24697  mbfadd  24730  mbfsub  24731  mbflimsup  24735  0plef  24741  itg1climres  24784  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfmul  24796  xrge0f  24801  itg2ge0  24805  itg2seq  24812  itg2uba  24813  itg2lea  24814  itg2eqa  24815  itg2splitlem  24818  itg2split  24819  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  bddmulibl  24908  ellimc3  24948  dvaddbr  25007  dvcobr  25015  dvcj  25019  dvfre  25020  dvcnvlem  25045  dvlip  25062  dvlipcn  25063  c1lip1  25066  tdeglem4  25129  tdeglem4OLD  25130  tdeglem2  25131  coe1mul3  25169  ply1rem  25233  fta1g  25237  ig1pdvds  25246  plyf  25264  plyeq0lem  25276  plypf1  25278  plyaddlem  25281  plymullem  25282  plyco  25307  dgreq  25310  0dgrb  25312  coefv0  25314  coeaddlem  25315  coemullem  25316  coemulc  25321  plycn  25327  dgrcolem2  25340  plycjlem  25342  plycj  25343  plyrecj  25345  plyreres  25348  dvply1  25349  vieta1lem2  25376  vieta1  25377  elqaalem2  25385  aareccl  25391  aalioulem1  25397  ulmcaulem  25458  ulmcau  25459  ulmcn  25463  mtest  25468  psergf  25476  dvradcnv  25485  psercn2  25487  pserdvlem2  25492  pserdv2  25494  abelthlem6  25500  abelthlem8  25503  abelthlem9  25504  logtayl  25720  amgm  26045  ftalem1  26127  ftalem2  26128  ftalem3  26129  ftalem4  26130  ftalem5  26131  basellem2  26136  muinv  26247  dchrmulcl  26302  dchrinvcl  26306  dchrfi  26308  dchrghm  26309  dchrsum2  26321  dchrsum  26322  bposlem5  26341  lgscllem  26357  lgsval4a  26372  lgsneg  26374  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgseisenlem3  26430  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumiflem1  26554  dchrisum0ff  26560  dchrisum0flblem1  26561  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem2a  26570  upgrreslem  27574  umgrreslem  27575  wlkpvtx  27929  wlkepvtx  27930  usgr2pthlem  28032  frgrncvvdeqlem8  28571  lnoadd  29021  lnosub  29022  nmosetre  29027  nmooge0  29030  nmoub3i  29036  nmounbi  29039  phoeqi  29120  ubthlem1  29133  h2hcau  29242  h2hlm  29243  hoscl  30008  homcl  30009  hodcl  30010  hoaddcl  30021  homulcl  30022  homulid2  30063  homco1  30064  homulass  30065  hoadddi  30066  hoadddir  30067  hoeq1  30093  hoeq2  30094  adjsym  30096  nmopsetretALT  30126  nmfnsetre  30140  cnvadj  30155  hhcno  30167  hhcnf  30168  nmopub2tALT  30172  nmopge0  30174  unopf1o  30179  unoplin  30183  counop  30184  nmfnleub2  30189  nmfnge0  30190  hmoplin  30205  eigvalcl  30224  lnop0  30229  hmops  30283  hmopm  30284  nlelchi  30324  leop2  30387  leopadd  30395  leopmuli  30396  leopnmid  30401  hmopidmchi  30414  pjinvari  30454  sticl  30478  fcomptf  30897  rge0scvg  31801  esumcst  31931  esumfzf  31937  esumfsup  31938  esumfsupre  31939  hasheuni  31953  measdivcstALTV  32093  eulerpartlems  32227  eulerpartlemgc  32229  eulerpartlemb  32235  derangsn  33032  subfacp1lem5  33046  subfacp1lem6  33047  pconnconn  33093  sconnpi1  33101  txsconnlem  33102  cvxsconn  33105  cvmliftphtlem  33179  cvmlift3lem2  33182  cvmlift3lem4  33184  cvmlift3lem6  33186  satfvel  33274  satefvfmla1  33287  elmrsubrn  33382  msubff  33392  msubvrs  33422  mclsssvlem  33424  faclim  33618  soseq  33730  curf  35682  uncf  35683  curunc  35686  unccur  35687  matunitlindflem1  35700  matunitlindflem2  35701  ptrecube  35704  heicant  35739  mblfinlem2  35742  itg2addnclem  35755  ftc1anclem1  35777  ftc1anclem2  35778  ftc1anclem4  35780  upixp  35814  fdc  35830  seqpo  35832  incsequz  35833  incsequz2  35834  metf1o  35840  geomcau  35844  sstotbnd2  35859  prdsbnd  35878  ismtyima  35888  ismtyhmeolem  35889  heiborlem3  35898  heiborlem6  35901  heiborlem10  35905  bfplem1  35907  ghomco  35976  sticksstones11  40040  mzpclall  40465  mzprename  40487  rexrabdioph  40532  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  expdioph  40761  pw2f1ocnv  40775  kelac1  40804  rngunsnply  40914  ofsubid  41831  ofdivrec  41833  ofdivcan4  41834  ofdivdiv2  41835  dvconstbi  41841  refsum2cnlem1  42469  dffo3f  42606  climinf  43037  stoweidlem26  43457  stoweidlem60  43491  stoweid  43494  dmvolsal  43775  caratheodory  43956  elhoi  43970  smfresal  44209  f1oresf1o2  44670  fargshiftf  44780  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  isomushgr  45166  isomgrtrlem  45178  mgmhmpropd  45227  rmsupp0  45592  domnmsuppn0  45593  gsumlsscl  45607  lincfsuppcl  45642  linccl  45643  lincdifsn  45653  lincsum  45658  lincscm  45659  lincscmcl  45661  lincext1  45683  lindslinindimp2lem1  45687  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  snlindsntor  45700  lincresunitlem2  45705  lincresunit3lem1  45708  lincresunit3lem2  45709  lincresunit3  45710  lincreslvec3  45711  isldepslvec2  45714  zlmodzxzldeplem3  45731  1arympt1  45872  ackendofnn0  45918  aacllem  46391