Theorem ffvelcdmi 7107

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 7105	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 703	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ⟶wf 6554  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566

This theorem is used by:  f0cli  7122  cantnfval2  9697  cantnfle  9699  cantnflt  9700  cantnfres  9705  cantnfp1lem3  9708  cantnflem1b  9714  cantnflem1d  9716  cantnflem1  9717  wemapwe  9725  cnfcomlem  9727  cnfcom  9728  cnfcom3lem  9731  cnfcom3  9732  ackbij1lem14  10337  ackbij1lem15  10338  ackbij1lem16  10339  ackbij1lem18  10341  fpwwe2lem7  10749  nqercl  11043  uzssz  13013  axdc4uzlem  14153  hashkf  14503  hashcl  14527  hashxrcl  14528  hashgadd  14548  cjcl  15301  limsupcl  15669  limsuplt  15675  limsupval2  15676  limsupgre  15677  limsupbnd2  15679  cn1lem  15794  climcn1lem  15799  caucvgrlem2  15871  fsumrelem  16003  ackbijnn  16026  efcl  16277  sincl  16323  coscl  16324  rpnnen2lem9  16419  rpnnen2lem12  16422  sadcaddlem  16656  sadadd2lem  16658  sadadd3  16660  sadaddlem  16665  sadasslem  16669  sadeq  16671  algcvg  16780  algcvgb  16782  algcvga  16783  algfx  16784  eucalgcvga  16790  eucalg  16791  xpsaddlem  17774  xpsvsca  17778  xpsle  17780  efgtf  19966  efgtlen  19970  efginvrel2  19971  efginvrel1  19972  efgsp1  19981  efgredleme  19987  efgredlemc  19989  efgred  19992  efgred2  19997  efgcpbllemb  19999  frgpnabllem1  20117  xpsdsval  24730  xrhmeo  25297  ioorcl  25928  volsup2  25956  volivth  25958  itg2const2  26092  itg2gt0  26111  dvcjbr  26299  dvcj  26300  dvfre  26301  rolle  26340  deg1xrcl  26430  plypf1  26561  resinf1o  26894  efif1olem4  26903  eff1olem  26906  logrncl  26925  relogcl  26933  asincl  27231  acoscl  27233  atancl  27239  asinrebnd  27259  dvatan  27293  leibpilem2  27299  leibpi  27300  areacl  27320  areage0  27321  divsqrtsumo1  27341  emcllem6  27358  emcllem7  27359  gamcl  27401  chtcl  27466  chpcl  27481  ppicl  27488  mucl  27498  sqff1o  27539  bposlem7  27647  dchrisum0lem2a  27874  mulog2sumlem1  27891  pntrsumo1  27922  pntrsumbnd  27923  pntrsumbnd2  27924  selbergr  27925  selberg3r  27926  selberg34r  27928  pntrlog2bndlem1  27934  pntrlog2bndlem2  27935  pntrlog2bndlem3  27936  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntrlog2bndlem6  27940  pntrlog2bnd  27941  pntpbnd1a  27942  pntpbnd1  27943  pntpbnd2  27944  pntibndlem2  27948  pntlemn  27957  pntlemj  27960  pntlemf  27962  pntlemo  27964  pntleml  27968  newf  28254  leftf  28271  rightf  28272  elmade  28273  sltsleft  28276  sltsright  28277  lnocoi  31389  nmlno0lem  31425  nmblolbii  31431  blocnilem  31436  blocni  31437  normcl  31757  occl  31936  hococli  32397  hosubcli  32401  hoaddcomi  32404  hodsi  32407  hoaddassi  32408  hocadddiri  32411  hocsubdiri  32412  ho2coi  32413  hoaddridi  32418  ho0coi  32420  hoid1ri  32422  honegsubi  32428  ho01i  32460  ho02i  32461  dmadjrn  32527  nmopnegi  32597  lnopaddi  32603  lnopsubi  32606  hoddii  32621  nmlnop0iALT  32627  lnopmi  32632  lnophsi  32633  lnopcoi  32635  lnopeq0lem1  32637  lnopeqi  32640  lnopunilem1  32642  lnopunilem2  32643  lnophmlem2  32649  nmbdoplbi  32656  nmcopexi  32659  nmcoplbi  32660  nmophmi  32663  lnopconi  32666  lnfn0i  32674  lnfnaddi  32675  lnfnmuli  32676  lnfnsubi  32678  nmbdfnlbi  32681  nmcfnexi  32683  nmcfnlbi  32684  lnfnconi  32687  riesz3i  32694  riesz4i  32695  cnlnadjlem2  32700  cnlnadjlem4  32702  cnlnadjlem6  32704  cnlnadjlem7  32705  nmopadjlem  32721  nmoptrii  32726  nmopcoi  32727  adjcoi  32732  nmopcoadji  32733  bracnln  32741  opsqrlem5  32776  opsqrlem6  32777  hmopidmchi  32783  hmopidmpji  32784  pjsdii  32787  pjddii  32788  pjcohocli  32835  mhmhmeotmd  34629  xrge0pluscn  34642  voliune  34932  volfiniune  34933  ddemeas  34939  eulerpartlems  35062  eulerpartlemsv3  35063  eulerpartlemgc  35064  eulerpartlemgvv  35078  eulerpartlemgf  35081  eulerpartlemgs2  35082  eulerpartlemn  35083  derangen  36104  subfacf  36107  subfacp1lem6  36117  subfaclim  36120  subfacval3  36121  msrrcl  36475  msrid  36477  circum  36606  fpwfvss  44605  hfstructwe  46234  liminfval2  46983  ismbl3  47201  ovolsplit  47203  stirlinglem13  47301  fourierdlem55  47376  fourierdlem77  47398  fourierdlem80  47401