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

Theorem fdmd 5352
Description: Deduction form of fdm 5351. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
fdmd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
fdmd (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fdmd
StepHypRef Expression
1 fdmd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 fdm 5351 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝜑 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  dom cdm 4609  wf 5192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-fn 5199  df-f 5200
This theorem is referenced by:  fssdmd  5359  fssdm  5360  ctssdccl  7084  1arith  12306  ennnfonelemg  12345  ennnfonelemrnh  12358  ennnfonelemf1  12360  ctinfomlemom  12369  ctinf  12372  lmbrf  12968  cnntri  12977  cncnp  12983  lmtopcnp  13003  txcnp  13024  hmeores  13068  xmetdmdm  13109  metn0  13131  ellimc3apf  13382  limccnpcntop  13397  dvfvalap  13403  dvcjbr  13425  dvcj  13426  dvfre  13427  dvexp  13428
  Copyright terms: Public domain W3C validator