Theorem fdmd 5356

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

Syntax hints:   → wi 4   = wceq 1349  dom cdm 4612  ⟶wf 5196

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 5203  df-f 5204

This theorem is referenced by:  fssdmd  5363  fssdm  5364  ctssdccl  7092  1arith  12323  ennnfonelemg  12362  ennnfonelemrnh  12375  ennnfonelemf1  12377  ctinfomlemom  12386  ctinf  12389  lmbrf  13094  cnntri  13103  cncnp  13109  lmtopcnp  13129  txcnp  13150  hmeores  13194  xmetdmdm  13235  metn0  13257  ellimc3apf  13508  limccnpcntop  13523  dvfvalap  13529  dvcjbr  13551  dvcj  13552  dvfre  13553  dvexp  13554