Theorem ffvelcdmi 7060

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

Syntax hints:   → wi 4   ∈ wcel 2141  ⟶wf 6513  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525

This theorem is referenced by:  f0cli  7075  cantnfval2  9621  cantnfle  9623  cantnflt  9624  cantnfres  9629  cantnfp1lem3  9632  cantnflem1b  9638  cantnflem1d  9640  cantnflem1  9641  wemapwe  9649  cnfcomlem  9651  cnfcom  9652  cnfcom3lem  9655  cnfcom3  9656  ackbij1lem14  10185  ackbij1lem15  10186  ackbij1lem16  10187  ackbij1lem18  10189  fpwwe2lem7  10592  nqercl  10886  uzssz  12857  axdc4uzlem  13993  hashkf  14342  hashcl  14366  hashxrcl  14367  hashgadd  14387  cjcl  15115  limsupcl  15483  limsuplt  15489  limsupval2  15490  limsupgre  15491  limsupbnd2  15493  cn1lem  15608  climcn1lem  15613  caucvgrlem2  15685  fsumrelem  15818  ackbijnn  15841  efcl  16095  sincl  16141  coscl  16142  rpnnen2lem9  16237  rpnnen2lem12  16240  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  algcvg  16593  algcvgb  16595  algcvga  16596  algfx  16597  eucalgcvga  16603  eucalg  16604  xpsaddlem  17586  xpsvsca  17590  xpsle  17592  efgtf  19745  efgtlen  19749  efginvrel2  19750  efginvrel1  19751  efgsp1  19760  efgredleme  19766  efgredlemc  19768  efgred  19771  efgred2  19776  efgcpbllemb  19778  frgpnabllem1  19896  xpsdsval  24421  xrhmeo  24988  ioorcl  25619  volsup2  25647  volivth  25649  itg2const2  25783  itg2gt0  25802  dvcjbr  25991  dvcj  25992  dvfre  25993  rolle  26032  deg1xrcl  26122  plypf1  26252  resinf1o  26578  efif1olem4  26587  eff1olem  26590  logrncl  26609  relogcl  26617  asincl  26915  acoscl  26917  atancl  26923  asinrebnd  26943  dvatan  26977  leibpilem2  26983  leibpi  26984  areacl  27004  areage0  27005  divsqrtsumo1  27025  emcllem6  27042  emcllem7  27043  gamcl  27085  chtcl  27150  chpcl  27165  ppicl  27172  mucl  27182  sqff1o  27223  bposlem7  27331  dchrisum0lem2a  27558  mulog2sumlem1  27575  pntrsumo1  27606  pntrsumbnd  27607  pntrsumbnd2  27608  selbergr  27609  selberg3r  27610  selberg34r  27612  pntrlog2bndlem1  27618  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntrlog2bndlem6  27624  pntrlog2bnd  27625  pntpbnd1a  27626  pntpbnd1  27627  pntpbnd2  27628  pntibndlem2  27632  pntlemn  27641  pntlemj  27644  pntlemf  27646  pntlemo  27648  pntleml  27652  newf  27908  leftf  27925  rightf  27926  elmade  27927  sltsleft  27930  sltsright  27931  lnocoi  30906  nmlno0lem  30942  nmblolbii  30948  blocnilem  30953  blocni  30954  normcl  31274  occl  31453  hococli  31914  hosubcli  31918  hoaddcomi  31921  hodsi  31924  hoaddassi  31925  hocadddiri  31928  hocsubdiri  31929  ho2coi  31930  hoaddridi  31935  ho0coi  31937  hoid1ri  31939  honegsubi  31945  ho01i  31977  ho02i  31978  dmadjrn  32044  nmopnegi  32114  lnopaddi  32120  lnopsubi  32123  hoddii  32138  nmlnop0iALT  32144  lnopmi  32149  lnophsi  32150  lnopcoi  32152  lnopeq0lem1  32154  lnopeqi  32157  lnopunilem1  32159  lnopunilem2  32160  lnophmlem2  32166  nmbdoplbi  32173  nmcopexi  32176  nmcoplbi  32177  nmophmi  32180  lnopconi  32183  lnfn0i  32191  lnfnaddi  32192  lnfnmuli  32193  lnfnsubi  32195  nmbdfnlbi  32198  nmcfnexi  32200  nmcfnlbi  32201  lnfnconi  32204  riesz3i  32211  riesz4i  32212  cnlnadjlem2  32217  cnlnadjlem4  32219  cnlnadjlem6  32221  cnlnadjlem7  32222  nmopadjlem  32238  nmoptrii  32243  nmopcoi  32244  adjcoi  32249  nmopcoadji  32250  bracnln  32258  opsqrlem5  32293  opsqrlem6  32294  hmopidmchi  32300  hmopidmpji  32301  pjsdii  32304  pjddii  32305  pjcohocli  32352  mhmhmeotmd  34185  xrge0pluscn  34198  voliune  34487  volfiniune  34488  ddemeas  34494  eulerpartlems  34618  eulerpartlemsv3  34619  eulerpartlemgc  34620  eulerpartlemgvv  34634  eulerpartlemgf  34637  eulerpartlemgs2  34638  eulerpartlemn  34639  derangen  35486  subfacf  35489  subfacp1lem6  35499  subfaclim  35502  subfacval3  35503  msrrcl  35857  msrid  35859  circum  35988  fpwfvss  43952  liminfval2  46306  ismbl3  46524  ovolsplit  46526  stirlinglem13  46624  fourierdlem55  46699  fourierdlem77  46721  fourierdlem80  46724