Theorem ffvelcdmi 7080

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

Syntax hints:   → wi 4   ∈ wcel 2143  ⟶wf 6534  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is referenced by:  f0cli  7095  cantnfval2  9639  cantnfle  9641  cantnflt  9642  cantnfres  9647  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1d  9658  cantnflem1  9659  wemapwe  9667  cnfcomlem  9669  cnfcom  9670  cnfcom3lem  9673  cnfcom3  9674  ackbij1lem14  10216  ackbij1lem15  10217  ackbij1lem16  10218  ackbij1lem18  10220  fpwwe2lem7  10623  nqercl  10917  uzssz  12884  axdc4uzlem  14021  hashkf  14370  hashcl  14394  hashxrcl  14395  hashgadd  14415  cjcl  15158  limsupcl  15526  limsuplt  15532  limsupval2  15533  limsupgre  15534  limsupbnd2  15536  cn1lem  15651  climcn1lem  15656  caucvgrlem2  15728  fsumrelem  15861  ackbijnn  15884  efcl  16137  sincl  16183  coscl  16184  rpnnen2lem9  16279  rpnnen2lem12  16282  sadcaddlem  16516  sadadd2lem  16518  sadadd3  16520  sadaddlem  16525  sadasslem  16529  sadeq  16531  algcvg  16635  algcvgb  16637  algcvga  16638  algfx  16639  eucalgcvga  16645  eucalg  16646  xpsaddlem  17628  xpsvsca  17632  xpsle  17634  efgtf  19793  efgtlen  19797  efginvrel2  19798  efginvrel1  19799  efgsp1  19808  efgredleme  19814  efgredlemc  19816  efgred  19819  efgred2  19824  efgcpbllemb  19826  frgpnabllem1  19944  xpsdsval  24519  xrhmeo  25086  ioorcl  25717  volsup2  25745  volivth  25747  itg2const2  25881  itg2gt0  25900  dvcjbr  26089  dvcj  26090  dvfre  26091  rolle  26130  deg1xrcl  26220  plypf1  26350  resinf1o  26679  efif1olem4  26688  eff1olem  26691  logrncl  26710  relogcl  26718  asincl  27016  acoscl  27018  atancl  27024  asinrebnd  27044  dvatan  27078  leibpilem2  27084  leibpi  27085  areacl  27105  areage0  27106  divsqrtsumo1  27126  emcllem6  27143  emcllem7  27144  gamcl  27186  chtcl  27251  chpcl  27266  ppicl  27273  mucl  27283  sqff1o  27324  bposlem7  27432  dchrisum0lem2a  27659  mulog2sumlem1  27676  pntrsumo1  27707  pntrsumbnd  27708  pntrsumbnd2  27709  selbergr  27710  selberg3r  27711  selberg34r  27713  pntrlog2bndlem1  27719  pntrlog2bndlem2  27720  pntrlog2bndlem3  27721  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntrlog2bndlem6  27725  pntrlog2bnd  27726  pntpbnd1a  27727  pntpbnd1  27728  pntpbnd2  27729  pntibndlem2  27733  pntlemn  27742  pntlemj  27745  pntlemf  27747  pntlemo  27749  pntleml  27753  newf  28009  leftf  28026  rightf  28027  elmade  28028  sltsleft  28031  sltsright  28032  lnocoi  31087  nmlno0lem  31123  nmblolbii  31129  blocnilem  31134  blocni  31135  normcl  31455  occl  31634  hococli  32095  hosubcli  32099  hoaddcomi  32102  hodsi  32105  hoaddassi  32106  hocadddiri  32109  hocsubdiri  32110  ho2coi  32111  hoaddridi  32116  ho0coi  32118  hoid1ri  32120  honegsubi  32126  ho01i  32158  ho02i  32159  dmadjrn  32225  nmopnegi  32295  lnopaddi  32301  lnopsubi  32304  hoddii  32319  nmlnop0iALT  32325  lnopmi  32330  lnophsi  32331  lnopcoi  32333  lnopeq0lem1  32335  lnopeqi  32338  lnopunilem1  32340  lnopunilem2  32341  lnophmlem2  32347  nmbdoplbi  32354  nmcopexi  32357  nmcoplbi  32358  nmophmi  32361  lnopconi  32364  lnfn0i  32372  lnfnaddi  32373  lnfnmuli  32374  lnfnsubi  32376  nmbdfnlbi  32379  nmcfnexi  32381  nmcfnlbi  32382  lnfnconi  32385  riesz3i  32392  riesz4i  32393  cnlnadjlem2  32398  cnlnadjlem4  32400  cnlnadjlem6  32402  cnlnadjlem7  32403  nmopadjlem  32419  nmoptrii  32424  nmopcoi  32425  adjcoi  32430  nmopcoadji  32431  bracnln  32439  opsqrlem5  32474  opsqrlem6  32475  hmopidmchi  32481  hmopidmpji  32482  pjsdii  32485  pjddii  32486  pjcohocli  32533  mhmhmeotmd  34295  xrge0pluscn  34308  voliune  34597  volfiniune  34598  ddemeas  34604  eulerpartlems  34728  eulerpartlemsv3  34729  eulerpartlemgc  34730  eulerpartlemgvv  34744  eulerpartlemgf  34747  eulerpartlemgs2  34748  eulerpartlemn  34749  derangen  35642  subfacf  35645  subfacp1lem6  35655  subfaclim  35658  subfacval3  35659  msrrcl  36013  msrid  36015  circum  36144  fpwfvss  44118  liminfval2  46462  ismbl3  46680  ovolsplit  46682  stirlinglem13  46780  fourierdlem55  46855  fourierdlem77  46877  fourierdlem80  46880