Theorem fdmd 5344

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

Syntax hints:   → wi 4   = wceq 1343  dom cdm 4604  ⟶wf 5184

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 5191  df-f 5192

This theorem is referenced by:  fssdmd  5351  fssdm  5352  ctssdccl  7076  1arith  12297  ennnfonelemg  12336  ennnfonelemrnh  12349  ennnfonelemf1  12351  ctinfomlemom  12360  ctinf  12363  lmbrf  12855  cnntri  12864  cncnp  12870  lmtopcnp  12890  txcnp  12911  hmeores  12955  xmetdmdm  12996  metn0  13018  ellimc3apf  13269  limccnpcntop  13284  dvfvalap  13290  dvcjbr  13312  dvcj  13313  dvfre  13314  dvexp  13315