Theorem fdmd 5486

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723  ⟶wf 5320

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 5327  df-f 5328

This theorem is referenced by:  fssdmd  5493  fssdm  5494  ctssdccl  7304  wrddm  11114  swrdclg  11224  cats1un  11295  s2dmg  11364  1arith  12933  ennnfonelemg  13017  ennnfonelemrnh  13030  ennnfonelemf1  13032  ctinfomlemom  13041  ctinf  13044  igsumval  13466  ghmrn  13837  psrbaglesuppg  14679  psrbagfi  14680  lmbrf  14932  cnntri  14941  cncnp  14947  lmtopcnp  14967  txcnp  14988  hmeores  15032  xmetdmdm  15073  metn0  15095  ellimc3apf  15377  limccnpcntop  15392  dvfvalap  15398  dvcjbr  15425  dvcj  15426  dvfre  15427  dvexp  15428  plyaddlem1  15464  plymullem1  15465  plycoeid3  15474  wrdupgren  15940  wrdumgren  15950  gfsumval  16630