Theorem fdmd 5483

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4720  ⟶wf 5317

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 5324  df-f 5325

This theorem is referenced by:  fssdmd  5490  fssdm  5491  ctssdccl  7294  wrddm  11097  swrdclg  11203  cats1un  11274  s2dmg  11343  1arith  12911  ennnfonelemg  12995  ennnfonelemrnh  13008  ennnfonelemf1  13010  ctinfomlemom  13019  ctinf  13022  igsumval  13444  ghmrn  13815  psrbaglesuppg  14657  psrbagfi  14658  lmbrf  14910  cnntri  14919  cncnp  14925  lmtopcnp  14945  txcnp  14966  hmeores  15010  xmetdmdm  15051  metn0  15073  ellimc3apf  15355  limccnpcntop  15370  dvfvalap  15376  dvcjbr  15403  dvcj  15404  dvfre  15405  dvexp  15406  plyaddlem1  15442  plymullem1  15443  plycoeid3  15452  wrdupgren  15917  wrdumgren  15927