Theorem fdmd 5384

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

Syntax hints:   → wi 4   = wceq 1363  dom cdm 4638  ⟶wf 5224

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 5231  df-f 5232

This theorem is referenced by:  fssdmd  5391  fssdm  5392  ctssdccl  7124  1arith  12379  ennnfonelemg  12418  ennnfonelemrnh  12431  ennnfonelemf1  12433  ctinfomlemom  12442  ctinf  12445  lmbrf  14011  cnntri  14020  cncnp  14026  lmtopcnp  14046  txcnp  14067  hmeores  14111  xmetdmdm  14152  metn0  14174  ellimc3apf  14425  limccnpcntop  14440  dvfvalap  14446  dvcjbr  14468  dvcj  14469  dvfre  14470  dvexp  14471