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

Theorem fdmd 5279
 Description: Deduction form of fdm 5278. 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 5278 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝜑 → dom 𝐹 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331  dom cdm 4539  ⟶wf 5119 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 5126  df-f 5127 This theorem is referenced by:  fssdmd  5286  fssdm  5287  ctssdccl  6996  ennnfonelemg  11922  ennnfonelemrnh  11935  ennnfonelemf1  11937  ctinfomlemom  11946  ctinf  11949  lmbrf  12393  cnntri  12402  cncnp  12408  lmtopcnp  12428  txcnp  12449  hmeores  12493  xmetdmdm  12534  metn0  12556  ellimc3apf  12807  limccnpcntop  12822  dvfvalap  12828  dvcjbr  12850  dvcj  12851  dvfre  12852  dvexp  12853
 Copyright terms: Public domain W3C validator