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

Theorem ffdmd 6523
 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 6522 . . 3 (𝐹:𝐴𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
31, 2syl 17 . 2 (𝜑 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
43simpld 499 1 (𝜑𝐹:dom 𝐹𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3859  dom cdm 5525  ⟶wf 6332 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876  df-fn 6339  df-f 6340 This theorem is referenced by:  ordtypelem5  9012  ablfaclem2  19269  ablfac2  19272  f1lindf  20580  lmcnp  21997  upgr1e  26998  upgrres1  27195  umgrres1  27196  umgr2v2e  27407  pliguhgr  28361  s3f1  30738  ccatf1  30740  swrdf1  30745  tocyccntz  30930  dfac21  40376  xlimmnfvlem1  42833  xlimpnfvlem1  42837  itgperiod  42982  issmfd  43728  issmfdf  43730  cnfsmf  43733  issmfled  43750  issmfgtd  43753  smfsuplem1  43801
 Copyright terms: Public domain W3C validator