Theorem ffvelcdmi 7075

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ⟶wf 6527  ‘cfv 6531

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is used by:  f0cli  7090  cantnfval2  9654  cantnfle  9656  cantnflt  9657  cantnfres  9662  cantnfp1lem3  9665  cantnflem1b  9671  cantnflem1d  9673  cantnflem1  9674  wemapwe  9682  cnfcomlem  9684  cnfcom  9685  cnfcom3lem  9688  cnfcom3  9689  ackbij1lem14  10291  ackbij1lem15  10292  ackbij1lem16  10293  ackbij1lem18  10295  fpwwe2lem7  10703  nqercl  10997  uzssz  12967  axdc4uzlem  14106  hashkf  14456  hashcl  14480  hashxrcl  14481  hashgadd  14501  cjcl  15252  limsupcl  15620  limsuplt  15626  limsupval2  15627  limsupgre  15628  limsupbnd2  15630  cn1lem  15745  climcn1lem  15750  caucvgrlem2  15822  fsumrelem  15954  ackbijnn  15977  efcl  16228  sincl  16274  coscl  16275  rpnnen2lem9  16370  rpnnen2lem12  16373  sadcaddlem  16607  sadadd2lem  16609  sadadd3  16611  sadaddlem  16616  sadasslem  16620  sadeq  16622  algcvg  16731  algcvgb  16733  algcvga  16734  algfx  16735  eucalgcvga  16741  eucalg  16742  xpsaddlem  17725  xpsvsca  17729  xpsle  17731  efgtf  19916  efgtlen  19920  efginvrel2  19921  efginvrel1  19922  efgsp1  19931  efgredleme  19937  efgredlemc  19939  efgred  19942  efgred2  19947  efgcpbllemb  19949  frgpnabllem1  20067  xpsdsval  24680  xrhmeo  25247  ioorcl  25878  volsup2  25906  volivth  25908  itg2const2  26042  itg2gt0  26061  dvcjbr  26249  dvcj  26250  dvfre  26251  rolle  26290  deg1xrcl  26380  plypf1  26511  resinf1o  26846  efif1olem4  26855  eff1olem  26858  logrncl  26877  relogcl  26885  asincl  27183  acoscl  27185  atancl  27191  asinrebnd  27211  dvatan  27245  leibpilem2  27251  leibpi  27252  areacl  27272  areage0  27273  divsqrtsumo1  27293  emcllem6  27310  emcllem7  27311  gamcl  27353  chtcl  27418  chpcl  27433  ppicl  27440  mucl  27450  sqff1o  27491  bposlem7  27599  dchrisum0lem2a  27826  mulog2sumlem1  27843  pntrsumo1  27874  pntrsumbnd  27875  pntrsumbnd2  27876  selbergr  27877  selberg3r  27878  selberg34r  27880  pntrlog2bndlem1  27886  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntrlog2bndlem6  27892  pntrlog2bnd  27893  pntpbnd1a  27894  pntpbnd1  27895  pntpbnd2  27896  pntibndlem2  27900  pntlemn  27909  pntlemj  27912  pntlemf  27914  pntlemo  27916  pntleml  27920  newf  28206  leftf  28223  rightf  28224  elmade  28225  sltsleft  28228  sltsright  28229  lnocoi  31341  nmlno0lem  31377  nmblolbii  31383  blocnilem  31388  blocni  31389  normcl  31709  occl  31888  hococli  32349  hosubcli  32353  hoaddcomi  32356  hodsi  32359  hoaddassi  32360  hocadddiri  32363  hocsubdiri  32364  ho2coi  32365  hoaddridi  32370  ho0coi  32372  hoid1ri  32374  honegsubi  32380  ho01i  32412  ho02i  32413  dmadjrn  32479  nmopnegi  32549  lnopaddi  32555  lnopsubi  32558  hoddii  32573  nmlnop0iALT  32579  lnopmi  32584  lnophsi  32585  lnopcoi  32587  lnopeq0lem1  32589  lnopeqi  32592  lnopunilem1  32594  lnopunilem2  32595  lnophmlem2  32601  nmbdoplbi  32608  nmcopexi  32611  nmcoplbi  32612  nmophmi  32615  lnopconi  32618  lnfn0i  32626  lnfnaddi  32627  lnfnmuli  32628  lnfnsubi  32630  nmbdfnlbi  32633  nmcfnexi  32635  nmcfnlbi  32636  lnfnconi  32639  riesz3i  32646  riesz4i  32647  cnlnadjlem2  32652  cnlnadjlem4  32654  cnlnadjlem6  32656  cnlnadjlem7  32657  nmopadjlem  32673  nmoptrii  32678  nmopcoi  32679  adjcoi  32684  nmopcoadji  32685  bracnln  32693  opsqrlem5  32728  opsqrlem6  32729  hmopidmchi  32735  hmopidmpji  32736  pjsdii  32739  pjddii  32740  pjcohocli  32787  mhmhmeotmd  34541  xrge0pluscn  34554  voliune  34844  volfiniune  34845  ddemeas  34851  eulerpartlems  34975  eulerpartlemsv3  34976  eulerpartlemgc  34977  eulerpartlemgvv  34991  eulerpartlemgf  34994  eulerpartlemgs2  34995  eulerpartlemn  34996  derangen  35906  subfacf  35909  subfacp1lem6  35919  subfaclim  35922  subfacval3  35923  msrrcl  36277  msrid  36279  circum  36408  fpwfvss  44371  liminfval2  46722  ismbl3  46940  ovolsplit  46942  stirlinglem13  47040  fourierdlem55  47115  fourierdlem77  47137  fourierdlem80  47140