MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffdmd Structured version   Visualization version   GIF version

Theorem ffdmd 6530
Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
ffdmd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
ffdmd (𝜑𝐹:dom 𝐹𝐵)

Proof of Theorem ffdmd
StepHypRef Expression
1 ffdmd.1 . . 3 (𝜑𝐹:𝐴𝐵)
2 ffdm 6529 . . 3 (𝐹:𝐴𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
31, 2syl 17 . 2 (𝜑 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
43simpld 497 1 (𝜑𝐹:dom 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wss 3934  dom cdm 5548  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950  df-fn 6351  df-f 6352
This theorem is referenced by:  ordtypelem5  8978  ablfaclem2  19200  ablfac2  19203  f1lindf  20958  lmcnp  21904  upgr1e  26890  upgrres1  27087  umgrres1  27088  umgr2v2e  27299  pliguhgr  28255  s3f1  30616  ccatf1  30618  swrdf1  30623  tocyccntz  30779  dfac21  39657  xlimmnfvlem1  42103  xlimpnfvlem1  42107  itgperiod  42256  issmfd  43003  issmfdf  43005  cnfsmf  43008  issmfled  43025  issmfgtd  43028  smfsuplem1  43076
  Copyright terms: Public domain W3C validator