ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fdmd Unicode version

Theorem fdmd 5367
Description: Deduction form of fdm 5366. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
fdmd.1  |-  ( ph  ->  F : A --> B )
Assertion
Ref Expression
fdmd  |-  ( ph  ->  dom  F  =  A )

Proof of Theorem fdmd
StepHypRef Expression
1 fdmd.1 . 2  |-  ( ph  ->  F : A --> B )
2 fdm 5366 . 2  |-  ( F : A --> B  ->  dom  F  =  A )
31, 2syl 14 1  |-  ( ph  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353   dom cdm 4622   -->wf 5207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-fn 5214  df-f 5215
This theorem is referenced by:  fssdmd  5374  fssdm  5375  ctssdccl  7103  1arith  12335  ennnfonelemg  12374  ennnfonelemrnh  12387  ennnfonelemf1  12389  ctinfomlemom  12398  ctinf  12401  lmbrf  13348  cnntri  13357  cncnp  13363  lmtopcnp  13383  txcnp  13404  hmeores  13448  xmetdmdm  13489  metn0  13511  ellimc3apf  13762  limccnpcntop  13777  dvfvalap  13783  dvcjbr  13805  dvcj  13806  dvfre  13807  dvexp  13808
  Copyright terms: Public domain W3C validator