Theorem fdmd 5456

Description: Deduction form of fdm 5455. 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

Step	Hyp	Ref	Expression
1		fdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fdm 5455	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1375  dom cdm 4696  ⟶wf 5290

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 5297  df-f 5298

This theorem is referenced by:  fssdmd  5463  fssdm  5464  ctssdccl  7246  wrddm  11046  swrdclg  11148  cats1un  11219  s2dmg  11288  1arith  12856  ennnfonelemg  12940  ennnfonelemrnh  12953  ennnfonelemf1  12955  ctinfomlemom  12964  ctinf  12967  igsumval  13389  ghmrn  13760  psrbaglesuppg  14601  psrbagfi  14602  lmbrf  14854  cnntri  14863  cncnp  14869  lmtopcnp  14889  txcnp  14910  hmeores  14954  xmetdmdm  14995  metn0  15017  ellimc3apf  15299  limccnpcntop  15314  dvfvalap  15320  dvcjbr  15347  dvcj  15348  dvfre  15349  dvexp  15350  plyaddlem1  15386  plymullem1  15387  plycoeid3  15396  wrdupgren  15861  wrdumgren  15871