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  10962  1arith  12563  ennnfonelemg  12647  ennnfonelemrnh  12660  ennnfonelemf1  12662  ctinfomlemom  12671  ctinf  12674  igsumval  13094  ghmrn  13465  psrbaglesuppg  14304  lmbrf  14537  cnntri  14546  cncnp  14552  lmtopcnp  14572  txcnp  14593  hmeores  14637  xmetdmdm  14678  metn0  14700  ellimc3apf  14982  limccnpcntop  14997  dvfvalap  15003  dvcjbr  15030  dvcj  15031  dvfre  15032  dvexp  15033  plyaddlem1  15069  plymullem1  15070  plycoeid3  15079