Theorem fdmd 5388

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4641  ⟶wf 5228

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 5235  df-f 5236

This theorem is referenced by:  fssdmd  5395  fssdm  5396  ctssdccl  7130  1arith  12385  ennnfonelemg  12429  ennnfonelemrnh  12442  ennnfonelemf1  12444  ctinfomlemom  12453  ctinf  12456  ghmrn  13164  lmbrf  14127  cnntri  14136  cncnp  14142  lmtopcnp  14162  txcnp  14183  hmeores  14227  xmetdmdm  14268  metn0  14290  ellimc3apf  14541  limccnpcntop  14556  dvfvalap  14562  dvcjbr  14584  dvcj  14585  dvfre  14586  dvexp  14587