Theorem fdmd 5540

Description: Deduction form of fdm 5539. 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 5539	. 2 |- ( F : A --> B -> dom F = A )
3	1, 2	syl 14	1 |- ( ph -> dom F = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   dom cdm 4774   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fssdmd  5548  fssdm  5549  suppsnopdc  6490  ctssdccl  7451  hashf1lem1  11299  wrddm  11326  swrdclg  11436  cats1un  11507  s2dmg  11576  1arith  13166  ennnfonelemg  13343  ennnfonelemrnh  13356  ennnfonelemf1  13358  ctinfomlemom  13367  ctinf  13370  gzsumval  13759  ghmrn  14109  gsumvalfi  14201  psrbaglesuppg  15106  psrbagfi  15108  lmbrf  15365  cnntri  15374  cncnp  15380  lmtopcnp  15400  txcnp  15421  hmeores  15465  xmetdmdm  15506  metn0  15528  ellimc3apf  15810  limccnpcntop  15825  dvfvalap  15831  dvcjbr  15858  dvcj  15859  dvfre  15860  dvexp  15861  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  wrdupgren  16435  wrdumgren  16445