Theorem fdmd 5287

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

Syntax hints:   → wi 4   = wceq 1332  dom cdm 4547  ⟶wf 5127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5134  df-f 5135

This theorem is referenced by:  fssdmd  5294  fssdm  5295  ctssdccl  7004  ennnfonelemg  11952  ennnfonelemrnh  11965  ennnfonelemf1  11967  ctinfomlemom  11976  ctinf  11979  lmbrf  12423  cnntri  12432  cncnp  12438  lmtopcnp  12458  txcnp  12479  hmeores  12523  xmetdmdm  12564  metn0  12586  ellimc3apf  12837  limccnpcntop  12852  dvfvalap  12858  dvcjbr  12880  dvcj  12881  dvfre  12882  dvexp  12883