Theorem fdmd 5491

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4727  ⟶wf 5324

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 5331  df-f 5332

This theorem is referenced by:  fssdmd  5498  fssdm  5499  ctssdccl  7315  wrddm  11130  swrdclg  11240  cats1un  11311  s2dmg  11380  1arith  12963  ennnfonelemg  13047  ennnfonelemrnh  13060  ennnfonelemf1  13062  ctinfomlemom  13071  ctinf  13074  igsumval  13496  ghmrn  13867  psrbaglesuppg  14710  psrbagfi  14712  lmbrf  14968  cnntri  14977  cncnp  14983  lmtopcnp  15003  txcnp  15024  hmeores  15068  xmetdmdm  15109  metn0  15131  ellimc3apf  15413  limccnpcntop  15428  dvfvalap  15434  dvcjbr  15461  dvcj  15462  dvfre  15463  dvexp  15464  plyaddlem1  15500  plymullem1  15501  plycoeid3  15510  wrdupgren  15976  wrdumgren  15986  gfsumval  16748