Theorem ffvelcdmi 7085

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ⟶wf 6539  ‘cfv 6543

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 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is used by:  f0cli  7100  cantnfval2  9648  cantnfle  9650  cantnflt  9651  cantnfres  9656  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1d  9667  cantnflem1  9668  wemapwe  9676  cnfcomlem  9678  cnfcom  9679  cnfcom3lem  9682  cnfcom3  9683  ackbij1lem14  10234  ackbij1lem15  10235  ackbij1lem16  10236  ackbij1lem18  10238  fpwwe2lem7  10640  nqercl  10934  uzssz  12901  axdc4uzlem  14039  hashkf  14388  hashcl  14412  hashxrcl  14413  hashgadd  14433  cjcl  15182  limsupcl  15550  limsuplt  15556  limsupval2  15557  limsupgre  15558  limsupbnd2  15560  cn1lem  15675  climcn1lem  15680  caucvgrlem2  15752  fsumrelem  15885  ackbijnn  15908  efcl  16161  sincl  16207  coscl  16208  rpnnen2lem9  16303  rpnnen2lem12  16306  sadcaddlem  16540  sadadd2lem  16542  sadadd3  16544  sadaddlem  16549  sadasslem  16553  sadeq  16555  algcvg  16659  algcvgb  16661  algcvga  16662  algfx  16663  eucalgcvga  16669  eucalg  16670  xpsaddlem  17652  xpsvsca  17656  xpsle  17658  efgtf  19823  efgtlen  19827  efginvrel2  19828  efginvrel1  19829  efgsp1  19838  efgredleme  19844  efgredlemc  19846  efgred  19849  efgred2  19854  efgcpbllemb  19856  frgpnabllem1  19974  xpsdsval  24575  xrhmeo  25142  ioorcl  25773  volsup2  25801  volivth  25803  itg2const2  25937  itg2gt0  25956  dvcjbr  26145  dvcj  26146  dvfre  26147  rolle  26186  deg1xrcl  26276  plypf1  26406  resinf1o  26738  efif1olem4  26747  eff1olem  26750  logrncl  26769  relogcl  26777  asincl  27075  acoscl  27077  atancl  27083  asinrebnd  27103  dvatan  27137  leibpilem2  27143  leibpi  27144  areacl  27164  areage0  27165  divsqrtsumo1  27185  emcllem6  27202  emcllem7  27203  gamcl  27245  chtcl  27310  chpcl  27325  ppicl  27332  mucl  27342  sqff1o  27383  bposlem7  27491  dchrisum0lem2a  27718  mulog2sumlem1  27735  pntrsumo1  27766  pntrsumbnd  27767  pntrsumbnd2  27768  selbergr  27769  selberg3r  27770  selberg34r  27772  pntrlog2bndlem1  27778  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntrlog2bndlem6  27784  pntrlog2bnd  27785  pntpbnd1a  27786  pntpbnd1  27787  pntpbnd2  27788  pntibndlem2  27792  pntlemn  27801  pntlemj  27804  pntlemf  27806  pntlemo  27808  pntleml  27812  newf  28068  leftf  28085  rightf  28086  elmade  28087  sltsleft  28090  sltsright  28091  lnocoi  31146  nmlno0lem  31182  nmblolbii  31188  blocnilem  31193  blocni  31194  normcl  31514  occl  31693  hococli  32154  hosubcli  32158  hoaddcomi  32161  hodsi  32164  hoaddassi  32165  hocadddiri  32168  hocsubdiri  32169  ho2coi  32170  hoaddridi  32175  ho0coi  32177  hoid1ri  32179  honegsubi  32185  ho01i  32217  ho02i  32218  dmadjrn  32284  nmopnegi  32354  lnopaddi  32360  lnopsubi  32363  hoddii  32378  nmlnop0iALT  32384  lnopmi  32389  lnophsi  32390  lnopcoi  32392  lnopeq0lem1  32394  lnopeqi  32397  lnopunilem1  32399  lnopunilem2  32400  lnophmlem2  32406  nmbdoplbi  32413  nmcopexi  32416  nmcoplbi  32417  nmophmi  32420  lnopconi  32423  lnfn0i  32431  lnfnaddi  32432  lnfnmuli  32433  lnfnsubi  32435  nmbdfnlbi  32438  nmcfnexi  32440  nmcfnlbi  32441  lnfnconi  32444  riesz3i  32451  riesz4i  32452  cnlnadjlem2  32457  cnlnadjlem4  32459  cnlnadjlem6  32461  cnlnadjlem7  32462  nmopadjlem  32478  nmoptrii  32483  nmopcoi  32484  adjcoi  32489  nmopcoadji  32490  bracnln  32498  opsqrlem5  32533  opsqrlem6  32534  hmopidmchi  32540  hmopidmpji  32541  pjsdii  32544  pjddii  32545  pjcohocli  32592  mhmhmeotmd  34348  xrge0pluscn  34361  voliune  34651  volfiniune  34652  ddemeas  34658  eulerpartlems  34782  eulerpartlemsv3  34783  eulerpartlemgc  34784  eulerpartlemgvv  34798  eulerpartlemgf  34801  eulerpartlemgs2  34802  eulerpartlemn  34803  derangen  35685  subfacf  35688  subfacp1lem6  35698  subfaclim  35701  subfacval3  35702  msrrcl  36056  msrid  36058  circum  36187  fpwfvss  44179  liminfval2  46523  ismbl3  46741  ovolsplit  46743  stirlinglem13  46841  fourierdlem55  46916  fourierdlem77  46938  fourierdlem80  46941  crossp3i  50690