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

Theorem fdmd 5384
Description: Deduction form of fdm 5383. 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 5383 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝜑 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1363  dom cdm 4638  wf 5224
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 5231  df-f 5232
This theorem is referenced by:  fssdmd  5391  fssdm  5392  ctssdccl  7124  1arith  12379  ennnfonelemg  12418  ennnfonelemrnh  12431  ennnfonelemf1  12433  ctinfomlemom  12442  ctinf  12445  lmbrf  14011  cnntri  14020  cncnp  14026  lmtopcnp  14046  txcnp  14067  hmeores  14111  xmetdmdm  14152  metn0  14174  ellimc3apf  14425  limccnpcntop  14440  dvfvalap  14446  dvcjbr  14468  dvcj  14469  dvfre  14470  dvexp  14471
  Copyright terms: Public domain W3C validator