Theorem ffvelcdmi 7083

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvelcdmi.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
ffvelcdmi	⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmi

Step	Hyp	Ref	Expression
1		ffvelcdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelcdm 7081	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 703	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ⟶wf 6534  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  f0cli  7098  cantnfval2  9673  cantnfle  9675  cantnflt  9676  cantnfres  9681  cantnfp1lem3  9684  cantnflem1b  9690  cantnflem1d  9692  cantnflem1  9693  wemapwe  9701  cnfcomlem  9703  cnfcom  9704  cnfcom3lem  9707  cnfcom3  9708  ackbij1lem14  10313  ackbij1lem15  10314  ackbij1lem16  10315  ackbij1lem18  10317  fpwwe2lem7  10725  nqercl  11019  uzssz  12989  axdc4uzlem  14129  hashkf  14479  hashcl  14503  hashxrcl  14504  hashgadd  14524  cjcl  15277  limsupcl  15645  limsuplt  15651  limsupval2  15652  limsupgre  15653  limsupbnd2  15655  cn1lem  15770  climcn1lem  15775  caucvgrlem2  15847  fsumrelem  15979  ackbijnn  16002  efcl  16253  sincl  16299  coscl  16300  rpnnen2lem9  16395  rpnnen2lem12  16398  sadcaddlem  16632  sadadd2lem  16634  sadadd3  16636  sadaddlem  16641  sadasslem  16645  sadeq  16647  algcvg  16756  algcvgb  16758  algcvga  16759  algfx  16760  eucalgcvga  16766  eucalg  16767  xpsaddlem  17750  xpsvsca  17754  xpsle  17756  efgtf  19941  efgtlen  19945  efginvrel2  19946  efginvrel1  19947  efgsp1  19956  efgredleme  19962  efgredlemc  19964  efgred  19967  efgred2  19972  efgcpbllemb  19974  frgpnabllem1  20092  xpsdsval  24705  xrhmeo  25272  ioorcl  25903  volsup2  25931  volivth  25933  itg2const2  26067  itg2gt0  26086  dvcjbr  26274  dvcj  26275  dvfre  26276  rolle  26315  deg1xrcl  26405  plypf1  26536  resinf1o  26869  efif1olem4  26878  eff1olem  26881  logrncl  26900  relogcl  26908  asincl  27206  acoscl  27208  atancl  27214  asinrebnd  27234  dvatan  27268  leibpilem2  27274  leibpi  27275  areacl  27295  areage0  27296  divsqrtsumo1  27316  emcllem6  27333  emcllem7  27334  gamcl  27376  chtcl  27441  chpcl  27456  ppicl  27463  mucl  27473  sqff1o  27514  bposlem7  27622  dchrisum0lem2a  27849  mulog2sumlem1  27866  pntrsumo1  27897  pntrsumbnd  27898  pntrsumbnd2  27899  selbergr  27900  selberg3r  27901  selberg34r  27903  pntrlog2bndlem1  27909  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntrlog2bndlem6  27915  pntrlog2bnd  27916  pntpbnd1a  27917  pntpbnd1  27918  pntpbnd2  27919  pntibndlem2  27923  pntlemn  27932  pntlemj  27935  pntlemf  27937  pntlemo  27939  pntleml  27943  newf  28229  leftf  28246  rightf  28247  elmade  28248  sltsleft  28251  sltsright  28252  lnocoi  31364  nmlno0lem  31400  nmblolbii  31406  blocnilem  31411  blocni  31412  normcl  31732  occl  31911  hococli  32372  hosubcli  32376  hoaddcomi  32379  hodsi  32382  hoaddassi  32383  hocadddiri  32386  hocsubdiri  32387  ho2coi  32388  hoaddridi  32393  ho0coi  32395  hoid1ri  32397  honegsubi  32403  ho01i  32435  ho02i  32436  dmadjrn  32502  nmopnegi  32572  lnopaddi  32578  lnopsubi  32581  hoddii  32596  nmlnop0iALT  32602  lnopmi  32607  lnophsi  32608  lnopcoi  32610  lnopeq0lem1  32612  lnopeqi  32615  lnopunilem1  32617  lnopunilem2  32618  lnophmlem2  32624  nmbdoplbi  32631  nmcopexi  32634  nmcoplbi  32635  nmophmi  32638  lnopconi  32641  lnfn0i  32649  lnfnaddi  32650  lnfnmuli  32651  lnfnsubi  32653  nmbdfnlbi  32656  nmcfnexi  32658  nmcfnlbi  32659  lnfnconi  32662  riesz3i  32669  riesz4i  32670  cnlnadjlem2  32675  cnlnadjlem4  32677  cnlnadjlem6  32679  cnlnadjlem7  32680  nmopadjlem  32696  nmoptrii  32701  nmopcoi  32702  adjcoi  32707  nmopcoadji  32708  bracnln  32716  opsqrlem5  32751  opsqrlem6  32752  hmopidmchi  32758  hmopidmpji  32759  pjsdii  32762  pjddii  32763  pjcohocli  32810  mhmhmeotmd  34605  xrge0pluscn  34618  voliune  34908  volfiniune  34909  ddemeas  34915  eulerpartlems  35038  eulerpartlemsv3  35039  eulerpartlemgc  35040  eulerpartlemgvv  35054  eulerpartlemgf  35057  eulerpartlemgs2  35058  eulerpartlemn  35059  derangen  36023  subfacf  36026  subfacp1lem6  36036  subfaclim  36039  subfacval3  36040  msrrcl  36394  msrid  36396  circum  36525  fpwfvss  44506  liminfval2  46871  ismbl3  47089  ovolsplit  47091  stirlinglem13  47189  fourierdlem55  47264  fourierdlem77  47286  fourierdlem80  47289