Theorem fdmd 5538

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

Syntax hints:   → wi 4   = wceq 1402  dom cdm 4772  ⟶wf 5371

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 5378  df-f 5379

This theorem is referenced by:  fssdmd  5546  fssdm  5547  suppsnopdc  6484  ctssdccl  7445  hashf1lem1  11268  wrddm  11295  swrdclg  11405  cats1un  11476  s2dmg  11545  1arith  13129  ennnfonelemg  13277  ennnfonelemrnh  13290  ennnfonelemf1  13292  ctinfomlemom  13301  ctinf  13304  gzsumval  13693  ghmrn  14043  gsumvalfi  14135  psrbaglesuppg  15040  psrbagfi  15042  lmbrf  15299  cnntri  15308  cncnp  15314  lmtopcnp  15334  txcnp  15355  hmeores  15399  xmetdmdm  15440  metn0  15462  ellimc3apf  15744  limccnpcntop  15759  dvfvalap  15765  dvcjbr  15792  dvcj  15793  dvfre  15794  dvexp  15795  plyaddlem1  15831  plymullem1  15832  plycoeid3  15841  wrdupgren  16320  wrdumgren  16330