Theorem fdmd 5417

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4664  ⟶wf 5255

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 5262  df-f 5263

This theorem is referenced by:  fssdmd  5424  fssdm  5425  ctssdccl  7186  wrddm  10960  1arith  12561  ennnfonelemg  12645  ennnfonelemrnh  12658  ennnfonelemf1  12660  ctinfomlemom  12669  ctinf  12672  igsumval  13092  ghmrn  13463  psrbaglesuppg  14302  lmbrf  14535  cnntri  14544  cncnp  14550  lmtopcnp  14570  txcnp  14591  hmeores  14635  xmetdmdm  14676  metn0  14698  ellimc3apf  14980  limccnpcntop  14995  dvfvalap  15001  dvcjbr  15028  dvcj  15029  dvfre  15030  dvexp  15031  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077