Theorem ffvelcdmi 7068

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

Syntax hints:   → wi 4   ∈ wcel 2145  ⟶wf 6521  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533

This theorem is referenced by:  f0cli  7083  cantnfval2  9626  cantnfle  9628  cantnflt  9629  cantnfres  9634  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1d  9645  cantnflem1  9646  wemapwe  9654  cnfcomlem  9656  cnfcom  9657  cnfcom3lem  9660  cnfcom3  9661  ackbij1lem14  10203  ackbij1lem15  10204  ackbij1lem16  10205  ackbij1lem18  10207  fpwwe2lem7  10610  nqercl  10904  uzssz  12874  axdc4uzlem  14010  hashkf  14359  hashcl  14383  hashxrcl  14384  hashgadd  14404  cjcl  15146  limsupcl  15514  limsuplt  15520  limsupval2  15521  limsupgre  15522  limsupbnd2  15524  cn1lem  15639  climcn1lem  15644  caucvgrlem2  15716  fsumrelem  15849  ackbijnn  15872  efcl  16126  sincl  16172  coscl  16173  rpnnen2lem9  16268  rpnnen2lem12  16271  sadcaddlem  16505  sadadd2lem  16507  sadadd3  16509  sadaddlem  16514  sadasslem  16518  sadeq  16520  algcvg  16624  algcvgb  16626  algcvga  16627  algfx  16628  eucalgcvga  16634  eucalg  16635  xpsaddlem  17617  xpsvsca  17621  xpsle  17623  efgtf  19783  efgtlen  19787  efginvrel2  19788  efginvrel1  19789  efgsp1  19798  efgredleme  19804  efgredlemc  19806  efgred  19809  efgred2  19814  efgcpbllemb  19816  frgpnabllem1  19934  xpsdsval  24499  xrhmeo  25066  ioorcl  25697  volsup2  25725  volivth  25727  itg2const2  25861  itg2gt0  25880  dvcjbr  26069  dvcj  26070  dvfre  26071  rolle  26110  deg1xrcl  26200  plypf1  26330  resinf1o  26659  efif1olem4  26668  eff1olem  26671  logrncl  26690  relogcl  26698  asincl  26996  acoscl  26998  atancl  27004  asinrebnd  27024  dvatan  27058  leibpilem2  27064  leibpi  27065  areacl  27085  areage0  27086  divsqrtsumo1  27106  emcllem6  27123  emcllem7  27124  gamcl  27166  chtcl  27231  chpcl  27246  ppicl  27253  mucl  27263  sqff1o  27304  bposlem7  27412  dchrisum0lem2a  27639  mulog2sumlem1  27656  pntrsumo1  27687  pntrsumbnd  27688  pntrsumbnd2  27689  selbergr  27690  selberg3r  27691  selberg34r  27693  pntrlog2bndlem1  27699  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntrlog2bndlem6  27705  pntrlog2bnd  27706  pntpbnd1a  27707  pntpbnd1  27708  pntpbnd2  27709  pntibndlem2  27713  pntlemn  27722  pntlemj  27725  pntlemf  27727  pntlemo  27729  pntleml  27733  newf  27989  leftf  28006  rightf  28007  elmade  28008  sltsleft  28011  sltsright  28012  lnocoi  31018  nmlno0lem  31054  nmblolbii  31060  blocnilem  31065  blocni  31066  normcl  31386  occl  31565  hococli  32026  hosubcli  32030  hoaddcomi  32033  hodsi  32036  hoaddassi  32037  hocadddiri  32040  hocsubdiri  32041  ho2coi  32042  hoaddridi  32047  ho0coi  32049  hoid1ri  32051  honegsubi  32057  ho01i  32089  ho02i  32090  dmadjrn  32156  nmopnegi  32226  lnopaddi  32232  lnopsubi  32235  hoddii  32250  nmlnop0iALT  32256  lnopmi  32261  lnophsi  32262  lnopcoi  32264  lnopeq0lem1  32266  lnopeqi  32269  lnopunilem1  32271  lnopunilem2  32272  lnophmlem2  32278  nmbdoplbi  32285  nmcopexi  32288  nmcoplbi  32289  nmophmi  32292  lnopconi  32295  lnfn0i  32303  lnfnaddi  32304  lnfnmuli  32305  lnfnsubi  32307  nmbdfnlbi  32310  nmcfnexi  32312  nmcfnlbi  32313  lnfnconi  32316  riesz3i  32323  riesz4i  32324  cnlnadjlem2  32329  cnlnadjlem4  32331  cnlnadjlem6  32333  cnlnadjlem7  32334  nmopadjlem  32350  nmoptrii  32355  nmopcoi  32356  adjcoi  32361  nmopcoadji  32362  bracnln  32370  opsqrlem5  32405  opsqrlem6  32406  hmopidmchi  32412  hmopidmpji  32413  pjsdii  32416  pjddii  32417  pjcohocli  32464  mhmhmeotmd  34234  xrge0pluscn  34247  voliune  34536  volfiniune  34537  ddemeas  34543  eulerpartlems  34667  eulerpartlemsv3  34668  eulerpartlemgc  34669  eulerpartlemgvv  34683  eulerpartlemgf  34686  eulerpartlemgs2  34687  eulerpartlemn  34688  derangen  35535  subfacf  35538  subfacp1lem6  35548  subfaclim  35551  subfacval3  35552  msrrcl  35906  msrid  35908  circum  36037  fpwfvss  44000  liminfval2  46340  ismbl3  46558  ovolsplit  46560  stirlinglem13  46658  fourierdlem55  46733  fourierdlem77  46755  fourierdlem80  46758