Theorem fdmd 5514

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4748  ⟶wf 5347

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 5354  df-f 5355

This theorem is referenced by:  fssdmd  5522  fssdm  5523  suppsnopdc  6449  ctssdccl  7401  wrddm  11225  swrdclg  11335  cats1un  11406  s2dmg  11475  1arith  13058  ennnfonelemg  13143  ennnfonelemrnh  13156  ennnfonelemf1  13158  ctinfomlemom  13167  ctinf  13170  igsumval  13592  ghmrn  13963  psrbaglesuppg  14808  psrbagfi  14810  lmbrf  15067  cnntri  15076  cncnp  15082  lmtopcnp  15102  txcnp  15123  hmeores  15167  xmetdmdm  15208  metn0  15230  ellimc3apf  15512  limccnpcntop  15527  dvfvalap  15533  dvcjbr  15560  dvcj  15561  dvfre  15562  dvexp  15563  plyaddlem1  15599  plymullem1  15600  plycoeid3  15609  wrdupgren  16078  wrdumgren  16088  gfsumval  16848