Theorem ffvelcdmi 7083

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ⟶wf 6534  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  f0cli  7098  cantnfval2  9671  cantnfle  9673  cantnflt  9674  cantnfres  9679  cantnfp1lem3  9682  cantnflem1b  9688  cantnflem1d  9690  cantnflem1  9691  wemapwe  9699  cnfcomlem  9701  cnfcom  9702  cnfcom3lem  9705  cnfcom3  9706  ackbij1lem14  10311  ackbij1lem15  10312  ackbij1lem16  10313  ackbij1lem18  10315  fpwwe2lem7  10723  nqercl  11017  uzssz  12987  axdc4uzlem  14127  hashkf  14477  hashcl  14501  hashxrcl  14502  hashgadd  14522  cjcl  15273  limsupcl  15641  limsuplt  15647  limsupval2  15648  limsupgre  15649  limsupbnd2  15651  cn1lem  15766  climcn1lem  15771  caucvgrlem2  15843  fsumrelem  15975  ackbijnn  15998  efcl  16249  sincl  16295  coscl  16296  rpnnen2lem9  16391  rpnnen2lem12  16394  sadcaddlem  16628  sadadd2lem  16630  sadadd3  16632  sadaddlem  16637  sadasslem  16641  sadeq  16643  algcvg  16752  algcvgb  16754  algcvga  16755  algfx  16756  eucalgcvga  16762  eucalg  16763  xpsaddlem  17746  xpsvsca  17750  xpsle  17752  efgtf  19937  efgtlen  19941  efginvrel2  19942  efginvrel1  19943  efgsp1  19952  efgredleme  19958  efgredlemc  19960  efgred  19963  efgred2  19968  efgcpbllemb  19970  frgpnabllem1  20088  xpsdsval  24701  xrhmeo  25268  ioorcl  25899  volsup2  25927  volivth  25929  itg2const2  26063  itg2gt0  26082  dvcjbr  26270  dvcj  26271  dvfre  26272  rolle  26311  deg1xrcl  26401  plypf1  26532  resinf1o  26865  efif1olem4  26874  eff1olem  26877  logrncl  26896  relogcl  26904  asincl  27202  acoscl  27204  atancl  27210  asinrebnd  27230  dvatan  27264  leibpilem2  27270  leibpi  27271  areacl  27291  areage0  27292  divsqrtsumo1  27312  emcllem6  27329  emcllem7  27330  gamcl  27372  chtcl  27437  chpcl  27452  ppicl  27459  mucl  27469  sqff1o  27510  bposlem7  27618  dchrisum0lem2a  27845  mulog2sumlem1  27862  pntrsumo1  27893  pntrsumbnd  27894  pntrsumbnd2  27895  selbergr  27896  selberg3r  27897  selberg34r  27899  pntrlog2bndlem1  27905  pntrlog2bndlem2  27906  pntrlog2bndlem3  27907  pntrlog2bndlem4  27908  pntrlog2bndlem5  27909  pntrlog2bndlem6  27911  pntrlog2bnd  27912  pntpbnd1a  27913  pntpbnd1  27914  pntpbnd2  27915  pntibndlem2  27919  pntlemn  27928  pntlemj  27931  pntlemf  27933  pntlemo  27935  pntleml  27939  newf  28225  leftf  28242  rightf  28243  elmade  28244  sltsleft  28247  sltsright  28248  lnocoi  31360  nmlno0lem  31396  nmblolbii  31402  blocnilem  31407  blocni  31408  normcl  31728  occl  31907  hococli  32368  hosubcli  32372  hoaddcomi  32375  hodsi  32378  hoaddassi  32379  hocadddiri  32382  hocsubdiri  32383  ho2coi  32384  hoaddridi  32389  ho0coi  32391  hoid1ri  32393  honegsubi  32399  ho01i  32431  ho02i  32432  dmadjrn  32498  nmopnegi  32568  lnopaddi  32574  lnopsubi  32577  hoddii  32592  nmlnop0iALT  32598  lnopmi  32603  lnophsi  32604  lnopcoi  32606  lnopeq0lem1  32608  lnopeqi  32611  lnopunilem1  32613  lnopunilem2  32614  lnophmlem2  32620  nmbdoplbi  32627  nmcopexi  32630  nmcoplbi  32631  nmophmi  32634  lnopconi  32637  lnfn0i  32645  lnfnaddi  32646  lnfnmuli  32647  lnfnsubi  32649  nmbdfnlbi  32652  nmcfnexi  32654  nmcfnlbi  32655  lnfnconi  32658  riesz3i  32665  riesz4i  32666  cnlnadjlem2  32671  cnlnadjlem4  32673  cnlnadjlem6  32675  cnlnadjlem7  32676  nmopadjlem  32692  nmoptrii  32697  nmopcoi  32698  adjcoi  32703  nmopcoadji  32704  bracnln  32712  opsqrlem5  32747  opsqrlem6  32748  hmopidmchi  32754  hmopidmpji  32755  pjsdii  32758  pjddii  32759  pjcohocli  32806  mhmhmeotmd  34602  xrge0pluscn  34615  voliune  34905  volfiniune  34906  ddemeas  34912  eulerpartlems  35035  eulerpartlemsv3  35036  eulerpartlemgc  35037  eulerpartlemgvv  35051  eulerpartlemgf  35054  eulerpartlemgs2  35055  eulerpartlemn  35056  derangen  35980  subfacf  35983  subfacp1lem6  35993  subfaclim  35996  subfacval3  35997  msrrcl  36351  msrid  36353  circum  36482  fpwfvss  44457  liminfval2  46822  ismbl3  47040  ovolsplit  47042  stirlinglem13  47140  fourierdlem55  47215  fourierdlem77  47237  fourierdlem80  47240