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  7310  wrddm  11125  swrdclg  11235  cats1un  11306  s2dmg  11375  1arith  12958  ennnfonelemg  13042  ennnfonelemrnh  13055  ennnfonelemf1  13057  ctinfomlemom  13066  ctinf  13069  igsumval  13491  ghmrn  13862  psrbaglesuppg  14705  psrbagfi  14706  lmbrf  14958  cnntri  14967  cncnp  14973  lmtopcnp  14993  txcnp  15014  hmeores  15058  xmetdmdm  15099  metn0  15121  ellimc3apf  15403  limccnpcntop  15418  dvfvalap  15424  dvcjbr  15451  dvcj  15452  dvfre  15453  dvexp  15454  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  wrdupgren  15966  wrdumgren  15976  gfsumval  16732