Theorem fdmd 5452

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

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4693  ⟶wf 5286

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 5293  df-f 5294

This theorem is referenced by:  fssdmd  5459  fssdm  5460  ctssdccl  7239  wrddm  11039  swrdclg  11141  cats1un  11212  1arith  12805  ennnfonelemg  12889  ennnfonelemrnh  12902  ennnfonelemf1  12904  ctinfomlemom  12913  ctinf  12916  igsumval  13337  ghmrn  13708  psrbaglesuppg  14549  psrbagfi  14550  lmbrf  14802  cnntri  14811  cncnp  14817  lmtopcnp  14837  txcnp  14858  hmeores  14902  xmetdmdm  14943  metn0  14965  ellimc3apf  15247  limccnpcntop  15262  dvfvalap  15268  dvcjbr  15295  dvcj  15296  dvfre  15297  dvexp  15298  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  wrdupgren  15807  wrdumgren  15817