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

Theorem fdmd 5394
Description: Deduction form of fdm 5393. 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 5393 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝜑 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1364  dom cdm 4647  wf 5234
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 5241  df-f 5242
This theorem is referenced by:  fssdmd  5401  fssdm  5402  ctssdccl  7144  1arith  12410  ennnfonelemg  12465  ennnfonelemrnh  12478  ennnfonelemf1  12480  ctinfomlemom  12489  ctinf  12492  igsumval  12877  ghmrn  13221  psrbaglesuppg  13975  lmbrf  14200  cnntri  14209  cncnp  14215  lmtopcnp  14235  txcnp  14256  hmeores  14300  xmetdmdm  14341  metn0  14363  ellimc3apf  14614  limccnpcntop  14629  dvfvalap  14635  dvcjbr  14657  dvcj  14658  dvfre  14659  dvexp  14660
  Copyright terms: Public domain W3C validator