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

Theorem ffdmd 6735
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 6734 . . 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 3944  dom cdm 5669  wf 6528
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 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-fn 6535  df-f 6536
This theorem is referenced by:  ordtypelem5  9499  ablfaclem2  19915  ablfac2  19918  f1lindf  21310  lmcnp  22737  upgr1e  28238  upgrres1  28435  umgrres1  28436  umgr2v2e  28647  pliguhgr  29602  s3f1  31984  ccatf1  31986  swrdf1  31991  tocyccntz  32174  dfac21  41579  xlimmnfvlem1  44321  xlimpnfvlem1  44325  itgperiod  44470  issmfd  45224  issmfdf  45226  cnfsmf  45229  issmfled  45246  issmfgtd  45250  smfsuplem1  45300
  Copyright terms: Public domain W3C validator