Theorem fdmd 5543

Description: Deduction form of fdm 5542. 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 5542	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4776  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5383  df-f 5384

This theorem is used by:  fssdmd  5551  fssdm  5552  suppsnopdc  6494  ctssdccl  7458  hashf1lem1  11308  wrddm  11335  swrdclg  11445  cats1un  11516  s2dmg  11585  1arith  13176  ennnfonelemg  13353  ennnfonelemrnh  13366  ennnfonelemf1  13368  ctinfomlemom  13377  ctinf  13380  gzsumval  13770  ghmrn  14120  cntzmhm2  14175  gsumvalfi  14243  gsumresfi  14264  gsum2dfilem2  14273  psrbagfi  15168  psrbaglesuppg  15172  lmbrf  15453  cnntri  15462  cncnp  15468  lmtopcnp  15488  txcnp  15509  hmeores  15553  xmetdmdm  15594  metn0  15616  ellimc3apf  15898  limccnpcntop  15913  dvfvalap  15919  dvcjbr  15946  dvcj  15947  dvfre  15948  dvexp  15949  plyaddlem1  15985  plymullem1  15986  plycoeid3  15995  wrdupgren  16554  wrdumgren  16564