Theorem ffvelrn 6849

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 6514	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6848	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6520	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3966	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 483	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ran crn 5556   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  ffvelrni  6850  ffvelrnda  6851  dffo3  6868  foco2  6873  ffnfv  6882  ffvresb  6888  fcompt  6895  fsn2  6898  fvconst  6926  fprb  6956  f1cofveqaeq  7016  2f1fvneq  7018  fcofo  7044  cocan1  7047  isocnv  7083  isocnv3  7085  isores2  7086  isopolem  7098  isosolem  7100  fovrn  7318  off  7424  fnwelem  7825  smofvon2  7993  smorndom  8005  omsmolem  8280  omsmo  8281  mapfvd  8443  mapsncnv  8457  2dom  8582  xpdom2  8612  domunsncan  8617  xpmapenlem  8684  fiint  8795  infdifsn  9120  cantnflem1  9152  wemapwe  9160  cnfcom3lem  9166  updjudhf  9360  fseqenlem1  9450  finacn  9476  ackbij1lem12  9653  cofsmo  9691  cfsmolem  9692  cfcoflem  9694  coftr  9695  isf32lem6  9780  isf32lem7  9781  isf34lem7  9801  isf34lem6  9802  acncc  9862  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  ttukeylem6  9936  alephreg  10004  pwcfsdom  10005  canthp1lem2  10075  canthp1  10076  pwfseqlem1  10080  pwfseqlem4a  10083  gruf  10233  fsequb2  13345  axdc4uzlem  13352  seqf1o  13412  hashf1lem1  13814  wwlktovf  14320  shftf  14438  limsupgre  14838  rlimuni  14907  lo1resb  14921  o1resb  14923  o1of2  14969  o1rlimmul  14975  isercolllem1  15021  isercolllem2  15022  isercolllem3  15023  isercoll  15024  climsup  15026  iseralt  15041  sumeq2ii  15050  summolem2a  15072  isumcl  15116  isumshft  15194  climcndslem2  15205  climcnds  15206  mertenslem2  15241  prodeq2ii  15267  prodmolem2a  15288  iprodcl  15355  rpnnen2lem10  15576  ruclem8  15590  ruclem12  15594  3dvds  15680  smueqlem  15839  nn0seqcvgd  15914  algrf  15917  eucalg  15931  phimullem  16116  pcmpt  16228  pcprod  16231  vdwlem11  16327  vdwnnlem3  16333  ramlb  16355  0ram  16356  ramcl  16365  prmgaplem8  16394  imasaddfnlem  16801  imasaddflem  16803  mhmpropd  17962  smndex1gid  18068  ghmsub  18366  cntzmhm  18469  f1omvdconj  18574  pj1ghm  18829  gsumzaddlem  19041  gsumzadd  19042  gsummptnn0fzfv  19107  dprdfadd  19142  subgdmdprd  19156  gsumdixp  19359  lspcl  19748  psrbaglesupp  20148  psrbaglefi  20152  resspsrmul  20197  evlslem4  20288  evlslem3  20293  fvcoe1  20375  psropprmul  20406  00ply1bas  20408  subrgvr1cl  20430  coe1mul2lem1  20435  coe1tmmul  20445  ply1coe  20464  evl1val  20492  evl1sca  20497  pf1const  20509  znunit  20710  frlmsslsp  20940  frlmup2  20943  lindfmm  20971  islindf4  20982  1mavmul  21157  mavmulass  21158  marepvcl  21178  1marepvmarrepid  21184  cramerimplem1  21292  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  cpmadugsumlemF  21484  cpmadugsumfi  21485  cayleyhamilton1  21500  hauscmplem  22014  ptbasid  22183  ptpjcn  22219  upxp  22231  uptx  22233  txcmplem2  22250  xkopt  22263  txhmeo  22411  alexsubALTlem3  22657  nrginvrcn  23301  nmoi  23337  nmoleub  23340  cncfmet  23516  cnheibor  23559  evth  23563  pcopt  23626  pcopt2  23627  pcorevlem  23630  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  iscauf  23883  iscmet3lem1  23894  iscmet3lem2  23895  iscmet3  23896  causs  23901  bcthlem5  23931  bcth3  23934  ovolfcl  24067  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovolfsval  24071  ovolmge0  24078  ovollb2lem  24089  ovolunlem1a  24097  ovoliunlem1  24103  ovoliunlem2  24104  ovoliun  24106  ovolicc1  24117  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2lem5  24122  voliunlem1  24151  volsup  24157  ioombl1lem2  24160  ovolfs2  24172  uniioovol  24180  uniiccvol  24181  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  dyadmbl  24201  volcn  24207  ismbf  24229  mbfadd  24262  mbfsub  24263  mbflimsup  24267  0plef  24273  itg1climres  24315  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfmul  24327  xrge0f  24332  itg2ge0  24336  itg2seq  24343  itg2uba  24344  itg2lea  24345  itg2eqa  24346  itg2splitlem  24349  itg2split  24350  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  bddmulibl  24439  ellimc3  24477  dvaddbr  24535  dvcobr  24543  dvcj  24547  dvfre  24548  dvcnvlem  24573  dvlip  24590  dvlipcn  24591  c1lip1  24594  tdeglem4  24654  tdeglem2  24655  coe1mul3  24693  ply1rem  24757  fta1g  24761  ig1pdvds  24770  plyf  24788  plyeq0lem  24800  plypf1  24802  plyaddlem  24805  plymullem  24806  plyco  24831  dgreq  24834  0dgrb  24836  coefv0  24838  coeaddlem  24839  coemullem  24840  coemulc  24845  plycn  24851  dgrcolem2  24864  plycjlem  24866  plycj  24867  plyrecj  24869  plyreres  24872  dvply1  24873  vieta1lem2  24900  vieta1  24901  elqaalem2  24909  aareccl  24915  aalioulem1  24921  ulmcaulem  24982  ulmcau  24983  ulmcn  24987  mtest  24992  psergf  25000  dvradcnv  25009  psercn2  25011  pserdvlem2  25016  pserdv2  25018  abelthlem6  25024  abelthlem8  25027  abelthlem9  25028  logtayl  25243  amgm  25568  ftalem1  25650  ftalem2  25651  ftalem3  25652  ftalem4  25653  ftalem5  25654  basellem2  25659  muinv  25770  dchrmulcl  25825  dchrinvcl  25829  dchrfi  25831  dchrghm  25832  dchrsum2  25844  dchrsum  25845  bposlem5  25864  lgscllem  25880  lgsval4a  25895  lgsneg  25897  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  lgseisenlem3  25953  rpvmasumlem  26063  dchrmusum2  26070  dchrvmasumiflem1  26077  dchrisum0ff  26083  dchrisum0flblem1  26084  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem2a  26093  upgrreslem  27086  umgrreslem  27087  wlkpvtx  27441  wlkepvtx  27442  usgr2pthlem  27544  frgrncvvdeqlem8  28085  lnoadd  28535  lnosub  28536  nmosetre  28541  nmooge0  28544  nmoub3i  28550  nmounbi  28553  phoeqi  28634  ubthlem1  28647  h2hcau  28756  h2hlm  28757  hoscl  29522  homcl  29523  hodcl  29524  hoaddcl  29535  homulcl  29536  homulid2  29577  homco1  29578  homulass  29579  hoadddi  29580  hoadddir  29581  hoeq1  29607  hoeq2  29608  adjsym  29610  nmopsetretALT  29640  nmfnsetre  29654  cnvadj  29669  hhcno  29681  hhcnf  29682  nmopub2tALT  29686  nmopge0  29688  unopf1o  29693  unoplin  29697  counop  29698  nmfnleub2  29703  nmfnge0  29704  hmoplin  29719  eigvalcl  29738  lnop0  29743  hmops  29797  hmopm  29798  nlelchi  29838  leop2  29901  leopadd  29909  leopmuli  29910  leopnmid  29915  hmopidmchi  29928  pjinvari  29968  sticl  29992  fcomptf  30403  rge0scvg  31192  esumcst  31322  esumfzf  31328  esumfsup  31329  esumfsupre  31330  hasheuni  31344  measdivcstALTV  31484  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemb  31626  derangsn  32417  subfacp1lem5  32431  subfacp1lem6  32432  pconnconn  32478  sconnpi1  32486  txsconnlem  32487  cvxsconn  32490  cvmliftphtlem  32564  cvmlift3lem2  32567  cvmlift3lem4  32569  cvmlift3lem6  32571  satfvel  32659  satefvfmla1  32672  elmrsubrn  32767  msubff  32777  msubvrs  32807  mclsssvlem  32809  faclim  32978  soseq  33096  curf  34885  uncf  34886  curunc  34889  unccur  34890  matunitlindflem1  34903  matunitlindflem2  34904  ptrecube  34907  heicant  34942  mblfinlem2  34945  itg2addnclem  34958  ftc1anclem1  34982  ftc1anclem2  34983  ftc1anclem4  34985  upixp  35019  fdc  35035  seqpo  35037  incsequz  35038  incsequz2  35039  metf1o  35045  geomcau  35049  sstotbnd2  35067  prdsbnd  35086  ismtyima  35096  ismtyhmeolem  35097  heiborlem3  35106  heiborlem6  35109  heiborlem10  35113  bfplem1  35115  ghomco  35184  mzpclall  39373  mzprename  39395  rexrabdioph  39440  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  expdioph  39669  pw2f1ocnv  39683  kelac1  39712  rngunsnply  39822  ofsubid  40705  ofdivrec  40707  ofdivcan4  40708  ofdivdiv2  40709  dvconstbi  40715  refsum2cnlem1  41343  dffo3f  41487  climinf  41936  stoweidlem26  42360  stoweidlem60  42394  stoweid  42397  dmvolsal  42678  caratheodory  42859  elhoi  42873  smfresal  43112  f1oresf1o2  43539  fargshiftf  43649  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  isomushgr  44040  isomgrtrlem  44052  mgmhmpropd  44101  rmsupp0  44465  domnmsuppn0  44466  gsumlsscl  44480  lincfsuppcl  44517  linccl  44518  lincdifsn  44528  lincsum  44533  lincscm  44534  lincscmcl  44536  lincext1  44558  lindslinindimp2lem1  44562  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  snlindsntor  44575  lincresunitlem2  44580  lincresunit3lem1  44583  lincresunit3lem2  44584  lincresunit3  44585  lincreslvec3  44586  isldepslvec2  44589  zlmodzxzldeplem3  44606  aacllem  44951