Theorem fdmd 5517

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4751  ⟶wf 5350

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 5357  df-f 5358

This theorem is referenced by:  fssdmd  5525  fssdm  5526  suppsnopdc  6452  ctssdccl  7404  wrddm  11240  swrdclg  11350  cats1un  11421  s2dmg  11490  1arith  13073  ennnfonelemg  13175  ennnfonelemrnh  13188  ennnfonelemf1  13190  ctinfomlemom  13199  ctinf  13202  igsumval  13624  ghmrn  13995  psrbaglesuppg  14870  psrbagfi  14872  lmbrf  15129  cnntri  15138  cncnp  15144  lmtopcnp  15164  txcnp  15185  hmeores  15229  xmetdmdm  15270  metn0  15292  ellimc3apf  15574  limccnpcntop  15589  dvfvalap  15595  dvcjbr  15622  dvcj  15623  dvfre  15624  dvexp  15625  plyaddlem1  15661  plymullem1  15662  plycoeid3  15671  wrdupgren  16140  wrdumgren  16150  gfsumval  16911