Theorem fdmd 5373

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4627  ⟶wf 5213

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 5220  df-f 5221

This theorem is referenced by:  fssdmd  5380  fssdm  5381  ctssdccl  7110  1arith  12365  ennnfonelemg  12404  ennnfonelemrnh  12417  ennnfonelemf1  12419  ctinfomlemom  12428  ctinf  12431  lmbrf  13718  cnntri  13727  cncnp  13733  lmtopcnp  13753  txcnp  13774  hmeores  13818  xmetdmdm  13859  metn0  13881  ellimc3apf  14132  limccnpcntop  14147  dvfvalap  14153  dvcjbr  14175  dvcj  14176  dvfre  14177  dvexp  14178