Theorem ffvelcdmi 7028

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

Syntax hints:   → wi 4   ∈ wcel 2113  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  f0cli  7043  cantnfval2  9578  cantnfle  9580  cantnflt  9581  cantnfres  9586  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1d  9597  cantnflem1  9598  wemapwe  9606  cnfcomlem  9608  cnfcom  9609  cnfcom3lem  9612  cnfcom3  9613  ackbij1lem14  10142  ackbij1lem15  10143  ackbij1lem16  10144  ackbij1lem18  10146  fpwwe2lem7  10548  nqercl  10842  uzssz  12772  axdc4uzlem  13906  hashkf  14255  hashcl  14279  hashxrcl  14280  hashgadd  14300  cjcl  15028  limsupcl  15396  limsuplt  15402  limsupval2  15403  limsupgre  15404  limsupbnd2  15406  cn1lem  15521  climcn1lem  15526  caucvgrlem2  15598  fsumrelem  15730  ackbijnn  15751  efcl  16005  sincl  16051  coscl  16052  rpnnen2lem9  16147  rpnnen2lem12  16150  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  algcvg  16503  algcvgb  16505  algcvga  16506  algfx  16507  eucalgcvga  16513  eucalg  16514  xpsaddlem  17494  xpsvsca  17498  xpsle  17500  efgtf  19651  efgtlen  19655  efginvrel2  19656  efginvrel1  19657  efgsp1  19666  efgredleme  19672  efgredlemc  19674  efgred  19677  efgred2  19682  efgcpbllemb  19684  frgpnabllem1  19802  xpsdsval  24325  xrhmeo  24900  ioorcl  25534  volsup2  25562  volivth  25564  itg2const2  25698  itg2gt0  25717  dvcjbr  25909  dvcj  25910  dvfre  25911  rolle  25950  deg1xrcl  26043  plypf1  26173  resinf1o  26501  efif1olem4  26510  eff1olem  26513  logrncl  26532  relogcl  26540  asincl  26839  acoscl  26841  atancl  26847  asinrebnd  26867  dvatan  26901  leibpilem2  26907  leibpi  26908  areacl  26928  areage0  26929  divsqrtsumo1  26950  emcllem6  26967  emcllem7  26968  gamcl  27010  chtcl  27075  chpcl  27090  ppicl  27097  mucl  27107  sqff1o  27148  bposlem7  27257  dchrisum0lem2a  27484  mulog2sumlem1  27501  pntrsumo1  27532  pntrsumbnd  27533  pntrsumbnd2  27534  selbergr  27535  selberg3r  27536  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem2  27558  pntlemn  27567  pntlemj  27570  pntlemf  27572  pntlemo  27574  pntleml  27578  newf  27834  leftf  27851  rightf  27852  elmade  27853  sltsleft  27856  sltsright  27857  lnocoi  30832  nmlno0lem  30868  nmblolbii  30874  blocnilem  30879  blocni  30880  normcl  31200  occl  31379  hococli  31840  hosubcli  31844  hoaddcomi  31847  hodsi  31850  hoaddassi  31851  hocadddiri  31854  hocsubdiri  31855  ho2coi  31856  hoaddridi  31861  ho0coi  31863  hoid1ri  31865  honegsubi  31871  ho01i  31903  ho02i  31904  dmadjrn  31970  nmopnegi  32040  lnopaddi  32046  lnopsubi  32049  hoddii  32064  nmlnop0iALT  32070  lnopmi  32075  lnophsi  32076  lnopcoi  32078  lnopeq0lem1  32080  lnopeqi  32083  lnopunilem1  32085  lnopunilem2  32086  lnophmlem2  32092  nmbdoplbi  32099  nmcopexi  32102  nmcoplbi  32103  nmophmi  32106  lnopconi  32109  lnfn0i  32117  lnfnaddi  32118  lnfnmuli  32119  lnfnsubi  32121  nmbdfnlbi  32124  nmcfnexi  32126  nmcfnlbi  32127  lnfnconi  32130  riesz3i  32137  riesz4i  32138  cnlnadjlem2  32143  cnlnadjlem4  32145  cnlnadjlem6  32147  cnlnadjlem7  32148  nmopadjlem  32164  nmoptrii  32169  nmopcoi  32170  adjcoi  32175  nmopcoadji  32176  bracnln  32184  opsqrlem5  32219  opsqrlem6  32220  hmopidmchi  32226  hmopidmpji  32227  pjsdii  32230  pjddii  32231  pjcohocli  32278  mhmhmeotmd  34084  xrge0pluscn  34097  voliune  34386  volfiniune  34387  ddemeas  34393  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemgc  34519  eulerpartlemgvv  34533  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  derangen  35366  subfacf  35369  subfacp1lem6  35379  subfaclim  35382  subfacval3  35383  msrrcl  35737  msrid  35739  circum  35868  fpwfvss  43649  liminfval2  46008  ismbl3  46226  ovolsplit  46228  stirlinglem13  46326  fourierdlem55  46401  fourierdlem77  46423  fourierdlem80  46426