Theorem fdmd 5480

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4719  ⟶wf 5314

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 5321  df-f 5322

This theorem is referenced by:  fssdmd  5487  fssdm  5488  ctssdccl  7286  wrddm  11087  swrdclg  11190  cats1un  11261  s2dmg  11330  1arith  12898  ennnfonelemg  12982  ennnfonelemrnh  12995  ennnfonelemf1  12997  ctinfomlemom  13006  ctinf  13009  igsumval  13431  ghmrn  13802  psrbaglesuppg  14644  psrbagfi  14645  lmbrf  14897  cnntri  14906  cncnp  14912  lmtopcnp  14932  txcnp  14953  hmeores  14997  xmetdmdm  15038  metn0  15060  ellimc3apf  15342  limccnpcntop  15357  dvfvalap  15363  dvcjbr  15390  dvcj  15391  dvfre  15392  dvexp  15393  plyaddlem1  15429  plymullem1  15430  plycoeid3  15439  wrdupgren  15904  wrdumgren  15914