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 703	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ⟶wf 6533  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  f0cli  7095  cantnfval2  9652  cantnfle  9654  cantnflt  9655  cantnfres  9660  cantnfp1lem3  9663  cantnflem1b  9669  cantnflem1d  9671  cantnflem1  9672  wemapwe  9680  cnfcomlem  9682  cnfcom  9683  cnfcom3lem  9686  cnfcom3  9687  ackbij1lem14  10238  ackbij1lem15  10239  ackbij1lem16  10240  ackbij1lem18  10242  fpwwe2lem7  10650  nqercl  10944  uzssz  12912  axdc4uzlem  14051  hashkf  14400  hashcl  14424  hashxrcl  14425  hashgadd  14445  cjcl  15196  limsupcl  15564  limsuplt  15570  limsupval2  15571  limsupgre  15572  limsupbnd2  15574  cn1lem  15689  climcn1lem  15694  caucvgrlem2  15766  fsumrelem  15898  ackbijnn  15921  efcl  16174  sincl  16220  coscl  16221  rpnnen2lem9  16316  rpnnen2lem12  16319  sadcaddlem  16553  sadadd2lem  16555  sadadd3  16557  sadaddlem  16562  sadasslem  16566  sadeq  16568  algcvg  16672  algcvgb  16674  algcvga  16675  algfx  16676  eucalgcvga  16682  eucalg  16683  xpsaddlem  17665  xpsvsca  17669  xpsle  17671  efgtf  19855  efgtlen  19859  efginvrel2  19860  efginvrel1  19861  efgsp1  19870  efgredleme  19876  efgredlemc  19878  efgred  19881  efgred2  19886  efgcpbllemb  19888  frgpnabllem1  20006  xpsdsval  24613  xrhmeo  25180  ioorcl  25811  volsup2  25839  volivth  25841  itg2const2  25975  itg2gt0  25994  dvcjbr  26183  dvcj  26184  dvfre  26185  rolle  26224  deg1xrcl  26314  plypf1  26445  resinf1o  26781  efif1olem4  26790  eff1olem  26793  logrncl  26812  relogcl  26820  asincl  27118  acoscl  27120  atancl  27126  asinrebnd  27146  dvatan  27180  leibpilem2  27186  leibpi  27187  areacl  27207  areage0  27208  divsqrtsumo1  27228  emcllem6  27245  emcllem7  27246  gamcl  27288  chtcl  27353  chpcl  27368  ppicl  27375  mucl  27385  sqff1o  27426  bposlem7  27534  dchrisum0lem2a  27761  mulog2sumlem1  27778  pntrsumo1  27809  pntrsumbnd  27810  pntrsumbnd2  27811  selbergr  27812  selberg3r  27813  selberg34r  27815  pntrlog2bndlem1  27821  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntrlog2bnd  27828  pntpbnd1a  27829  pntpbnd1  27830  pntpbnd2  27831  pntibndlem2  27835  pntlemn  27844  pntlemj  27847  pntlemf  27849  pntlemo  27851  pntleml  27855  newf  28111  leftf  28128  rightf  28129  elmade  28130  sltsleft  28133  sltsright  28134  lnocoi  31246  nmlno0lem  31282  nmblolbii  31288  blocnilem  31293  blocni  31294  normcl  31614  occl  31793  hococli  32254  hosubcli  32258  hoaddcomi  32261  hodsi  32264  hoaddassi  32265  hocadddiri  32268  hocsubdiri  32269  ho2coi  32270  hoaddridi  32275  ho0coi  32277  hoid1ri  32279  honegsubi  32285  ho01i  32317  ho02i  32318  dmadjrn  32384  nmopnegi  32454  lnopaddi  32460  lnopsubi  32463  hoddii  32478  nmlnop0iALT  32484  lnopmi  32489  lnophsi  32490  lnopcoi  32492  lnopeq0lem1  32494  lnopeqi  32497  lnopunilem1  32499  lnopunilem2  32500  lnophmlem2  32506  nmbdoplbi  32513  nmcopexi  32516  nmcoplbi  32517  nmophmi  32520  lnopconi  32523  lnfn0i  32531  lnfnaddi  32532  lnfnmuli  32533  lnfnsubi  32535  nmbdfnlbi  32538  nmcfnexi  32540  nmcfnlbi  32541  lnfnconi  32544  riesz3i  32551  riesz4i  32552  cnlnadjlem2  32557  cnlnadjlem4  32559  cnlnadjlem6  32561  cnlnadjlem7  32562  nmopadjlem  32578  nmoptrii  32583  nmopcoi  32584  adjcoi  32589  nmopcoadji  32590  bracnln  32598  opsqrlem5  32633  opsqrlem6  32634  hmopidmchi  32640  hmopidmpji  32641  pjsdii  32644  pjddii  32645  pjcohocli  32692  mhmhmeotmd  34445  xrge0pluscn  34458  voliune  34748  volfiniune  34749  ddemeas  34755  eulerpartlems  34879  eulerpartlemsv3  34880  eulerpartlemgc  34881  eulerpartlemgvv  34895  eulerpartlemgf  34898  eulerpartlemgs2  34899  eulerpartlemn  34900  derangen  35759  subfacf  35762  subfacp1lem6  35772  subfaclim  35775  subfacval3  35776  msrrcl  36130  msrid  36132  circum  36261  fpwfvss  44260  liminfval2  46604  ismbl3  46822  ovolsplit  46824  stirlinglem13  46922  fourierdlem55  46997  fourierdlem77  47019  fourierdlem80  47022