Theorem fdmd 5489

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725  ⟶wf 5322

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 5329  df-f 5330

This theorem is referenced by:  fssdmd  5496  fssdm  5497  ctssdccl  7310  wrddm  11122  swrdclg  11232  cats1un  11303  s2dmg  11372  1arith  12942  ennnfonelemg  13026  ennnfonelemrnh  13039  ennnfonelemf1  13041  ctinfomlemom  13050  ctinf  13053  igsumval  13475  ghmrn  13846  psrbaglesuppg  14689  psrbagfi  14690  lmbrf  14942  cnntri  14951  cncnp  14957  lmtopcnp  14977  txcnp  14998  hmeores  15042  xmetdmdm  15083  metn0  15105  ellimc3apf  15387  limccnpcntop  15402  dvfvalap  15408  dvcjbr  15435  dvcj  15436  dvfre  15437  dvexp  15438  plyaddlem1  15474  plymullem1  15475  plycoeid3  15484  wrdupgren  15950  wrdumgren  15960  gfsumval  16701