Theorem ffvelcdmi 7084

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

Syntax hints:   → wi 4   ∈ wcel 2104  ⟶wf 6538  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  f0cli  7098  cantnfval2  9666  cantnfle  9668  cantnflt  9669  cantnfres  9674  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1d  9685  cantnflem1  9686  wemapwe  9694  cnfcomlem  9696  cnfcom  9697  cnfcom3lem  9700  cnfcom3  9701  ackbij1lem14  10230  ackbij1lem15  10231  ackbij1lem16  10232  ackbij1lem18  10234  fpwwe2lem7  10634  nqercl  10928  uzssz  12847  axdc4uzlem  13952  hashkf  14296  hashcl  14320  hashxrcl  14321  hashgadd  14341  cjcl  15056  limsupcl  15421  limsuplt  15427  limsupval2  15428  limsupgre  15429  limsupbnd2  15431  cn1lem  15546  climcn1lem  15551  caucvgrlem2  15625  fsumrelem  15757  ackbijnn  15778  efcl  16030  sincl  16073  coscl  16074  rpnnen2lem9  16169  rpnnen2lem12  16172  sadcaddlem  16402  sadadd2lem  16404  sadadd3  16406  sadaddlem  16411  sadasslem  16415  sadeq  16417  algcvg  16517  algcvgb  16519  algcvga  16520  algfx  16521  eucalgcvga  16527  eucalg  16528  xpsaddlem  17523  xpsvsca  17527  xpsle  17529  efgtf  19631  efgtlen  19635  efginvrel2  19636  efginvrel1  19637  efgsp1  19646  efgredleme  19652  efgredlemc  19654  efgred  19657  efgred2  19662  efgcpbllemb  19664  frgpnabllem1  19782  xpsdsval  24107  xrhmeo  24691  ioorcl  25326  volsup2  25354  volivth  25356  itg2const2  25491  itg2gt0  25510  dvcjbr  25701  dvcj  25702  dvfre  25703  rolle  25742  deg1xrcl  25835  plypf1  25961  resinf1o  26281  efif1olem4  26290  eff1olem  26293  logrncl  26312  relogcl  26320  asincl  26614  acoscl  26616  atancl  26622  asinrebnd  26642  dvatan  26676  leibpilem2  26682  leibpi  26683  areacl  26703  areage0  26704  divsqrtsumo1  26724  emcllem6  26741  emcllem7  26742  gamcl  26784  chtcl  26849  chpcl  26864  ppicl  26871  mucl  26881  sqff1o  26922  bposlem7  27029  dchrisum0lem2a  27256  mulog2sumlem1  27273  pntrsumo1  27304  pntrsumbnd  27305  pntrsumbnd2  27306  selbergr  27307  selberg3r  27308  selberg34r  27310  pntrlog2bndlem1  27316  pntrlog2bndlem2  27317  pntrlog2bndlem3  27318  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntrlog2bnd  27323  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem2  27330  pntlemn  27339  pntlemj  27342  pntlemf  27344  pntlemo  27346  pntleml  27350  newf  27590  leftf  27597  rightf  27598  elmade  27599  ssltleft  27602  ssltright  27603  lnocoi  30277  nmlno0lem  30313  nmblolbii  30319  blocnilem  30324  blocni  30325  normcl  30645  occl  30824  hococli  31285  hosubcli  31289  hoaddcomi  31292  hodsi  31295  hoaddassi  31296  hocadddiri  31299  hocsubdiri  31300  ho2coi  31301  hoaddridi  31306  ho0coi  31308  hoid1ri  31310  honegsubi  31316  ho01i  31348  ho02i  31349  dmadjrn  31415  nmopnegi  31485  lnopaddi  31491  lnopsubi  31494  hoddii  31509  nmlnop0iALT  31515  lnopmi  31520  lnophsi  31521  lnopcoi  31523  lnopeq0lem1  31525  lnopeqi  31528  lnopunilem1  31530  lnopunilem2  31531  lnophmlem2  31537  nmbdoplbi  31544  nmcopexi  31547  nmcoplbi  31548  nmophmi  31551  lnopconi  31554  lnfn0i  31562  lnfnaddi  31563  lnfnmuli  31564  lnfnsubi  31566  nmbdfnlbi  31569  nmcfnexi  31571  nmcfnlbi  31572  lnfnconi  31575  riesz3i  31582  riesz4i  31583  cnlnadjlem2  31588  cnlnadjlem4  31590  cnlnadjlem6  31592  cnlnadjlem7  31593  nmopadjlem  31609  nmoptrii  31614  nmopcoi  31615  adjcoi  31620  nmopcoadji  31621  bracnln  31629  opsqrlem5  31664  opsqrlem6  31665  hmopidmchi  31671  hmopidmpji  31672  pjsdii  31675  pjddii  31676  pjcohocli  31723  mhmhmeotmd  33205  xrge0pluscn  33218  voliune  33525  volfiniune  33526  ddemeas  33532  eulerpartlems  33657  eulerpartlemsv3  33658  eulerpartlemgc  33659  eulerpartlemgvv  33673  eulerpartlemgf  33676  eulerpartlemgs2  33677  eulerpartlemn  33678  derangen  34461  subfacf  34464  subfacp1lem6  34474  subfaclim  34477  subfacval3  34478  msrrcl  34832  msrid  34834  circum  34957  fpwfvss  42465  liminfval2  44782  ismbl3  45000  ovolsplit  45002  stirlinglem13  45100  fourierdlem55  45175  fourierdlem77  45197  fourierdlem80  45200