Theorem fdmd 5414

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4663  ⟶wf 5254

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 5261  df-f 5262

This theorem is referenced by:  fssdmd  5421  fssdm  5422  ctssdccl  7177  wrddm  10943  1arith  12536  ennnfonelemg  12620  ennnfonelemrnh  12633  ennnfonelemf1  12635  ctinfomlemom  12644  ctinf  12647  igsumval  13033  ghmrn  13387  psrbaglesuppg  14226  lmbrf  14451  cnntri  14460  cncnp  14466  lmtopcnp  14486  txcnp  14507  hmeores  14551  xmetdmdm  14592  metn0  14614  ellimc3apf  14896  limccnpcntop  14911  dvfvalap  14917  dvcjbr  14944  dvcj  14945  dvfre  14946  dvexp  14947  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993