Theorem fdmd 5520

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754  ⟶wf 5353

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 5360  df-f 5361

This theorem is referenced by:  fssdmd  5528  fssdm  5529  suppsnopdc  6463  ctssdccl  7415  wrddm  11260  swrdclg  11370  cats1un  11441  s2dmg  11510  1arith  13093  ennnfonelemg  13241  ennnfonelemrnh  13254  ennnfonelemf1  13256  ctinfomlemom  13265  ctinf  13268  igsumval  13656  ghmrn  14013  gfsumval  14105  psrbaglesuppg  14950  psrbagfi  14952  lmbrf  15209  cnntri  15218  cncnp  15224  lmtopcnp  15244  txcnp  15265  hmeores  15309  xmetdmdm  15350  metn0  15372  ellimc3apf  15654  limccnpcntop  15669  dvfvalap  15675  dvcjbr  15702  dvcj  15703  dvfre  15704  dvexp  15705  plyaddlem1  15741  plymullem1  15742  plycoeid3  15751  wrdupgren  16220  wrdumgren  16230