Theorem fdmd 5394

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4647  ⟶wf 5234

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 5241  df-f 5242

This theorem is referenced by:  fssdmd  5401  fssdm  5402  ctssdccl  7144  1arith  12410  ennnfonelemg  12465  ennnfonelemrnh  12478  ennnfonelemf1  12480  ctinfomlemom  12489  ctinf  12492  igsumval  12877  ghmrn  13221  psrbaglesuppg  13975  lmbrf  14200  cnntri  14209  cncnp  14215  lmtopcnp  14235  txcnp  14256  hmeores  14300  xmetdmdm  14341  metn0  14363  ellimc3apf  14614  limccnpcntop  14629  dvfvalap  14635  dvcjbr  14657  dvcj  14658  dvfre  14659  dvexp  14660