Theorem fdmd 5489

Description: Deduction form of fdm 5488. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
fdmd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
fdmd	|- ( ph -> dom F = A )

Proof of Theorem fdmd

Step	Hyp	Ref	Expression
1		fdmd.1	. 2 |- ( ph -> F : A --> B )
2		fdm 5488	. 2 |- ( F : A --> B -> dom F = A )
3	1, 2	syl 14	1 |- ( ph -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1397   dom cdm 4725   -->wf 5322

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 5329  df-f 5330

This theorem is referenced by:  fssdmd  5496  fssdm  5497  ctssdccl  7309  wrddm  11120  swrdclg  11230  cats1un  11301  s2dmg  11370  1arith  12939  ennnfonelemg  13023  ennnfonelemrnh  13036  ennnfonelemf1  13038  ctinfomlemom  13047  ctinf  13050  igsumval  13472  ghmrn  13843  psrbaglesuppg  14685  psrbagfi  14686  lmbrf  14938  cnntri  14947  cncnp  14953  lmtopcnp  14973  txcnp  14994  hmeores  15038  xmetdmdm  15079  metn0  15101  ellimc3apf  15383  limccnpcntop  15398  dvfvalap  15404  dvcjbr  15431  dvcj  15432  dvfre  15433  dvexp  15434  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  wrdupgren  15946  wrdumgren  15956  gfsumval  16680