Theorem fdmd 5540

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fssdmd  5548  fssdm  5549  suppsnopdc  6490  ctssdccl  7451  hashf1lem1  11287  wrddm  11314  swrdclg  11424  cats1un  11495  s2dmg  11564  1arith  13148  ennnfonelemg  13296  ennnfonelemrnh  13309  ennnfonelemf1  13311  ctinfomlemom  13320  ctinf  13323  gzsumval  13712  ghmrn  14062  gsumvalfi  14154  psrbaglesuppg  15059  psrbagfi  15061  lmbrf  15318  cnntri  15327  cncnp  15333  lmtopcnp  15353  txcnp  15374  hmeores  15418  xmetdmdm  15459  metn0  15481  ellimc3apf  15763  limccnpcntop  15778  dvfvalap  15784  dvcjbr  15811  dvcj  15812  dvfre  15813  dvexp  15814  plyaddlem1  15850  plymullem1  15851  plycoeid3  15860  wrdupgren  16349  wrdumgren  16359