Theorem ffvelcdmi 7035

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6494  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  f0cli  7050  cantnfval2  9590  cantnfle  9592  cantnflt  9593  cantnfres  9598  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  wemapwe  9618  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  cnfcom3  9625  ackbij1lem14  10154  ackbij1lem15  10155  ackbij1lem16  10156  ackbij1lem18  10158  fpwwe2lem7  10560  nqercl  10854  uzssz  12809  axdc4uzlem  13945  hashkf  14294  hashcl  14318  hashxrcl  14319  hashgadd  14339  cjcl  15067  limsupcl  15435  limsuplt  15441  limsupval2  15442  limsupgre  15443  limsupbnd2  15445  cn1lem  15560  climcn1lem  15565  caucvgrlem2  15637  fsumrelem  15770  ackbijnn  15793  efcl  16047  sincl  16093  coscl  16094  rpnnen2lem9  16189  rpnnen2lem12  16192  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  algcvg  16545  algcvgb  16547  algcvga  16548  algfx  16549  eucalgcvga  16555  eucalg  16556  xpsaddlem  17537  xpsvsca  17541  xpsle  17543  efgtf  19697  efgtlen  19701  efginvrel2  19702  efginvrel1  19703  efgsp1  19712  efgredleme  19718  efgredlemc  19720  efgred  19723  efgred2  19728  efgcpbllemb  19730  frgpnabllem1  19848  xpsdsval  24346  xrhmeo  24913  ioorcl  25544  volsup2  25572  volivth  25574  itg2const2  25708  itg2gt0  25727  dvcjbr  25916  dvcj  25917  dvfre  25918  rolle  25957  deg1xrcl  26047  plypf1  26177  resinf1o  26500  efif1olem4  26509  eff1olem  26512  logrncl  26531  relogcl  26539  asincl  26837  acoscl  26839  atancl  26845  asinrebnd  26865  dvatan  26899  leibpilem2  26905  leibpi  26906  areacl  26926  areage0  26927  divsqrtsumo1  26947  emcllem6  26964  emcllem7  26965  gamcl  27007  chtcl  27072  chpcl  27087  ppicl  27094  mucl  27104  sqff1o  27145  bposlem7  27253  dchrisum0lem2a  27480  mulog2sumlem1  27497  pntrsumo1  27528  pntrsumbnd  27529  pntrsumbnd2  27530  selbergr  27531  selberg3r  27532  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntlemn  27563  pntlemj  27566  pntlemf  27568  pntlemo  27570  pntleml  27574  newf  27830  leftf  27847  rightf  27848  elmade  27849  sltsleft  27852  sltsright  27853  lnocoi  30828  nmlno0lem  30864  nmblolbii  30870  blocnilem  30875  blocni  30876  normcl  31196  occl  31375  hococli  31836  hosubcli  31840  hoaddcomi  31843  hodsi  31846  hoaddassi  31847  hocadddiri  31850  hocsubdiri  31851  ho2coi  31852  hoaddridi  31857  ho0coi  31859  hoid1ri  31861  honegsubi  31867  ho01i  31899  ho02i  31900  dmadjrn  31966  nmopnegi  32036  lnopaddi  32042  lnopsubi  32045  hoddii  32060  nmlnop0iALT  32066  lnopmi  32071  lnophsi  32072  lnopcoi  32074  lnopeq0lem1  32076  lnopeqi  32079  lnopunilem1  32081  lnopunilem2  32082  lnophmlem2  32088  nmbdoplbi  32095  nmcopexi  32098  nmcoplbi  32099  nmophmi  32102  lnopconi  32105  lnfn0i  32113  lnfnaddi  32114  lnfnmuli  32115  lnfnsubi  32117  nmbdfnlbi  32120  nmcfnexi  32122  nmcfnlbi  32123  lnfnconi  32126  riesz3i  32133  riesz4i  32134  cnlnadjlem2  32139  cnlnadjlem4  32141  cnlnadjlem6  32143  cnlnadjlem7  32144  nmopadjlem  32160  nmoptrii  32165  nmopcoi  32166  adjcoi  32171  nmopcoadji  32172  bracnln  32180  opsqrlem5  32215  opsqrlem6  32216  hmopidmchi  32222  hmopidmpji  32223  pjsdii  32226  pjddii  32227  pjcohocli  32274  mhmhmeotmd  34071  xrge0pluscn  34084  voliune  34373  volfiniune  34374  ddemeas  34380  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemgc  34506  eulerpartlemgvv  34520  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  derangen  35354  subfacf  35357  subfacp1lem6  35367  subfaclim  35370  subfacval3  35371  msrrcl  35725  msrid  35727  circum  35856  fpwfvss  43839  liminfval2  46196  ismbl3  46414  ovolsplit  46416  stirlinglem13  46514  fourierdlem55  46589  fourierdlem77  46611  fourierdlem80  46614