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

Theorem ffdmd 6700
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 6699 . . 3 (𝐹:𝐴𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
31, 2syl 17 . 2 (𝜑 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
43simpld 496 1 (𝜑𝐹:dom 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wss 3911  dom cdm 5634  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-fn 6500  df-f 6501
This theorem is referenced by:  ordtypelem5  9463  ablfaclem2  19870  ablfac2  19873  f1lindf  21244  lmcnp  22671  upgr1e  28106  upgrres1  28303  umgrres1  28304  umgr2v2e  28515  pliguhgr  29470  s3f1  31852  ccatf1  31854  swrdf1  31859  tocyccntz  32042  dfac21  41436  xlimmnfvlem1  44159  xlimpnfvlem1  44163  itgperiod  44308  issmfd  45062  issmfdf  45064  cnfsmf  45067  issmfled  45084  issmfgtd  45088  smfsuplem1  45138
  Copyright terms: Public domain W3C validator