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

Theorem ffdmd 6748
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 6747 . . 3 (𝐹:𝐴𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
31, 2syl 17 . 2 (𝜑 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
43simpld 495 1 (𝜑𝐹:dom 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3948  dom cdm 5676  wf 6539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-fn 6546  df-f 6547
This theorem is referenced by:  ordtypelem5  9516  ablfaclem2  19955  ablfac2  19958  f1lindf  21376  lmcnp  22807  upgr1e  28370  upgrres1  28567  umgrres1  28568  umgr2v2e  28779  pliguhgr  29734  s3f1  32108  ccatf1  32110  swrdf1  32115  tocyccntz  32298  dfac21  41798  xlimmnfvlem1  44538  xlimpnfvlem1  44542  itgperiod  44687  issmfd  45441  issmfdf  45443  cnfsmf  45446  issmfled  45463  issmfgtd  45467  smfsuplem1  45517
  Copyright terms: Public domain W3C validator