Theorem ffvelrn 6265

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ran crn 5039   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  ffvelrni  6266  ffvelrnda  6267  dffo3  6282  foco2  6287  foco2OLD  6288  ffnfv  6295  ffvresb  6301  fcompt  6306  fsn2  6309  fvconst  6336  fcofo  6443  cocan1  6446  isocnv  6480  isocnv3  6482  isores2  6483  isopolem  6495  isosolem  6497  fovrn  6702  off  6810  fnwelem  7179  smofvon2  7340  smorndom  7352  omsmolem  7620  omsmo  7621  mapsncnv  7790  2dom  7915  xpdom2  7940  domunsncan  7945  xpmapenlem  8012  fiint  8122  ordiso2  8303  infdifsn  8437  cantnflem1  8469  wemapwe  8477  cnfcom3lem  8483  fseqenlem1  8730  finacn  8756  ackbij1lem12  8936  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  coftr  8978  isf32lem6  9063  isf32lem7  9064  isf34lem7  9084  isf34lem6  9085  acncc  9145  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  ttukeylem6  9219  alephreg  9283  pwcfsdom  9284  canthp1lem2  9354  canthp1  9355  pwfseqlem1  9359  pwfseqlem4a  9362  gruf  9512  fsequb2  12637  axdc4uzlem  12644  seqf1o  12704  hashf1lem1  13096  wwlktovf  13547  shftf  13667  limsupgre  14060  rlimuni  14129  lo1resb  14143  o1resb  14145  o1of2  14191  o1rlimmul  14197  isercolllem1  14243  isercolllem2  14244  isercolllem3  14245  isercoll  14246  climsup  14248  iseralt  14263  sumeq2ii  14271  summolem2a  14293  isumcl  14334  isumshft  14410  climcndslem2  14421  climcnds  14422  mertenslem2  14456  prodeq2ii  14482  prodmolem2a  14503  iprodcl  14571  rpnnen2lem10  14791  ruclem8  14805  ruclem12  14809  3dvds  14890  3dvdsOLD  14891  smueqlem  15050  nn0seqcvgd  15121  algrf  15124  eucalg  15138  phimullem  15322  pcmpt  15434  pcprod  15437  vdwlem11  15533  vdwnnlem3  15539  ramlb  15561  0ram  15562  ramcl  15571  prmgaplem8  15600  imasaddfnlem  16011  imasaddflem  16013  mhmpropd  17164  ghmsub  17491  cntzmhm  17594  f1omvdconj  17689  pj1ghm  17939  gsumzaddlem  18144  gsumzadd  18145  gsummptnn0fzfv  18207  dprdfadd  18242  subgdmdprd  18256  gsumdixp  18432  lspcl  18797  psrbaglesupp  19189  psrbaglefi  19193  resspsrmul  19238  evlslem4  19329  evlslem3  19335  fvcoe1  19398  psropprmul  19429  00ply1bas  19431  subrgvr1cl  19453  coe1mul2lem1  19458  coe1tmmul  19468  ply1coe  19487  evl1val  19514  evl1sca  19519  pf1const  19531  znunit  19731  frlmsslsp  19954  frlmup2  19957  lindfmm  19985  islindf4  19996  1mavmul  20173  mavmulass  20174  marepvcl  20194  1marepvmarrepid  20200  cramerimplem1  20308  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  cpmadugsumlemF  20500  cpmadugsumfi  20501  cayleyhamilton1  20516  hauscmplem  21019  ptbasid  21188  ptpjcn  21224  upxp  21236  uptx  21238  txcmplem2  21255  xkopt  21268  txhmeo  21416  alexsubALTlem3  21663  nrginvrcn  22306  nmoi  22342  nmoleub  22345  cncfmet  22519  cnheibor  22562  evth  22566  pcopt  22630  pcopt2  22631  pcorevlem  22634  pi1xfrf  22661  pi1xfr  22663  pi1xfrcnvlem  22664  iscauf  22886  iscmet3lem1  22897  iscmet3lem2  22898  iscmet3  22899  causs  22904  bcthlem5  22933  bcth3  22936  ovolfcl  23042  ovolfioo  23043  ovolficc  23044  ovolficcss  23045  ovolfsval  23046  ovolmge0  23052  ovollb2lem  23063  ovolunlem1a  23071  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun  23080  ovolicc1  23091  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  voliunlem1  23125  volsup  23131  ioombl1lem2  23134  ovolfs2  23145  uniioovol  23153  uniiccvol  23154  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombllem6  23162  dyadmbl  23174  volcn  23180  ismbf  23203  mbfadd  23234  mbfsub  23235  mbflimsup  23239  0plef  23245  itg1climres  23287  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfmul  23299  xrge0f  23304  itg2ge0  23308  itg2seq  23315  itg2uba  23316  itg2lea  23317  itg2eqa  23318  itg2splitlem  23321  itg2split  23322  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  bddmulibl  23411  ellimc3  23449  dvaddbr  23507  dvcobr  23515  dvcj  23519  dvfre  23520  dvcnvlem  23543  dvlip  23560  dvlipcn  23561  c1lip1  23564  tdeglem4  23624  tdeglem2  23625  coe1mul3  23663  ply1rem  23727  fta1g  23731  ig1pdvds  23740  plyf  23758  plyeq0lem  23770  plypf1  23772  plyaddlem  23775  plymullem  23776  plyco  23801  dgreq  23804  0dgrb  23806  coefv0  23808  coeaddlem  23809  coemullem  23810  coemulc  23815  plycn  23821  dgrcolem2  23834  plycjlem  23836  plycj  23837  plyrecj  23839  plyreres  23842  dvply1  23843  vieta1lem2  23870  vieta1  23871  elqaalem2  23879  aareccl  23885  aalioulem1  23891  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  mtest  23962  psergf  23970  dvradcnv  23979  psercn2  23981  pserdvlem2  23986  pserdv2  23988  abelthlem6  23994  abelthlem8  23997  abelthlem9  23998  logtayl  24206  amgm  24517  ftalem1  24599  ftalem2  24600  ftalem3  24601  ftalem4  24602  ftalem5  24603  basellem2  24608  muinv  24719  dchrmulcl  24774  dchrinvcl  24778  dchrfi  24780  dchrghm  24781  dchrsum2  24793  dchrsum  24794  bposlem5  24813  lgscllem  24829  lgsval4a  24844  lgsneg  24846  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  lgseisenlem3  24902  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrisum0ff  24996  dchrisum0flblem1  24997  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem2a  25006  usgrarnedg  25913  usgraedg4  25916  usgrares1  25939  usgrwlknloop  26093  usgra2adedgwlkonALT  26144  usgra2wlkspthlem2  26148  cyclispthon  26161  fargshiftf  26164  usgrcyclnl2  26169  4cycl4dv  26195  el2wlkonotlem  26389  usg2wlkonot  26410  usg2wotspth  26411  vdgrnn0pnf  26436  frgrancvvdeqlemB  26565  lnoadd  26997  lnosub  26998  nmosetre  27003  nmooge0  27006  nmoub3i  27012  nmounbi  27015  phoeqi  27097  ubthlem1  27110  h2hcau  27220  h2hlm  27221  hoscl  27988  homcl  27989  hodcl  27990  hoaddcl  28001  homulcl  28002  homulid2  28043  homco1  28044  homulass  28045  hoadddi  28046  hoadddir  28047  hoeq1  28073  hoeq2  28074  adjsym  28076  nmopsetretALT  28106  nmfnsetre  28120  cnvadj  28135  hhcno  28147  hhcnf  28148  nmopub2tALT  28152  nmopge0  28154  unopf1o  28159  unoplin  28163  counop  28164  nmfnleub2  28169  nmfnge0  28170  hmoplin  28185  eigvalcl  28204  lnop0  28209  hmops  28263  hmopm  28264  nlelchi  28304  leop2  28367  leopadd  28375  leopmuli  28376  leopnmid  28381  hmopidmchi  28394  pjinvari  28434  sticl  28458  fcomptf  28840  rge0scvg  29323  esumcst  29452  esumfzf  29458  esumfsup  29459  esumfsupre  29460  hasheuni  29474  measdivcstOLD  29614  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemb  29757  derangsn  30406  subfacp1lem5  30420  subfacp1lem6  30421  pconcon  30467  sconpi1  30475  txsconlem  30476  cvxscon  30479  cvmliftphtlem  30553  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem6  30560  elmrsubrn  30671  msubff  30681  msubvrs  30711  mclsssvlem  30713  faclim  30885  fprb  30916  soseq  30995  curf  32557  uncf  32558  curunc  32561  unccur  32562  matunitlindflem1  32575  matunitlindflem2  32576  ptrecube  32579  heicant  32614  mblfinlem2  32617  itg2addnclem  32631  ftc1anclem1  32655  ftc1anclem2  32656  ftc1anclem4  32658  upixp  32694  fdc  32711  seqpo  32713  incsequz  32714  incsequz2  32715  metf1o  32721  geomcau  32725  sstotbnd2  32743  prdsbnd  32762  ismtyima  32772  ismtyhmeolem  32773  heiborlem3  32782  heiborlem6  32785  heiborlem10  32789  bfplem1  32791  ghomco  32860  mzpclall  36308  mzprename  36330  rexrabdioph  36376  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  pw2f1ocnv  36622  kelac1  36651  rngunsnply  36762  ofsubid  37545  ofdivrec  37547  ofdivcan4  37548  ofdivdiv2  37549  dvconstbi  37555  refsum2cnlem1  38219  dffo3f  38359  climinf  38673  stoweidlem26  38919  stoweidlem60  38953  stoweid  38956  dmvolsal  39240  caratheodory  39418  elhoi  39432  smfresal  39673  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  2f1fvneq  40322  f1cofveqaeq  40323  1wlkpvtx  40867  1wlkepvtx  40868  1wlkres  40879  usgr2pthlem  40969  frgrncvvdeqlemB  41477  mgmhmpropd  41575  rmsupp0  41943  domnmsuppn0  41944  gsumlsscl  41958  lincfsuppcl  41996  linccl  41997  lincdifsn  42007  lincsum  42012  lincscm  42013  lincscmcl  42015  lincext1  42037  lindslinindimp2lem1  42041  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  snlindsntor  42054  lincresunitlem2  42059  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064  lincreslvec3  42065  isldepslvec2  42068  zlmodzxzldeplem3  42085  aacllem  42356