Theorem fdmd 5352

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

Syntax hints:   → wi 4   = wceq 1348  dom cdm 4609  ⟶wf 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5199  df-f 5200

This theorem is referenced by:  fssdmd  5359  fssdm  5360  ctssdccl  7084  1arith  12306  ennnfonelemg  12345  ennnfonelemrnh  12358  ennnfonelemf1  12360  ctinfomlemom  12369  ctinf  12372  lmbrf  12968  cnntri  12977  cncnp  12983  lmtopcnp  13003  txcnp  13024  hmeores  13068  xmetdmdm  13109  metn0  13131  ellimc3apf  13382  limccnpcntop  13397  dvfvalap  13403  dvcjbr  13425  dvcj  13426  dvfre  13427  dvexp  13428