Theorem fdmd 5438

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

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4679  ⟶wf 5272

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 5279  df-f 5280

This theorem is referenced by:  fssdmd  5445  fssdm  5446  ctssdccl  7220  wrddm  11009  swrdclg  11111  1arith  12734  ennnfonelemg  12818  ennnfonelemrnh  12831  ennnfonelemf1  12833  ctinfomlemom  12842  ctinf  12845  igsumval  13266  ghmrn  13637  psrbaglesuppg  14478  psrbagfi  14479  lmbrf  14731  cnntri  14740  cncnp  14746  lmtopcnp  14766  txcnp  14787  hmeores  14831  xmetdmdm  14872  metn0  14894  ellimc3apf  15176  limccnpcntop  15191  dvfvalap  15197  dvcjbr  15224  dvcj  15225  dvfre  15226  dvexp  15227  plyaddlem1  15263  plymullem1  15264  plycoeid3  15273