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  11285  wrddm  11312  swrdclg  11422  cats1un  11493  s2dmg  11562  1arith  13146  ennnfonelemg  13294  ennnfonelemrnh  13307  ennnfonelemf1  13309  ctinfomlemom  13318  ctinf  13321  gzsumval  13710  ghmrn  14060  gsumvalfi  14152  psrbaglesuppg  15057  psrbagfi  15059  lmbrf  15316  cnntri  15325  cncnp  15331  lmtopcnp  15351  txcnp  15372  hmeores  15416  xmetdmdm  15457  metn0  15479  ellimc3apf  15761  limccnpcntop  15776  dvfvalap  15782  dvcjbr  15809  dvcj  15810  dvfre  15811  dvexp  15812  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  wrdupgren  16337  wrdumgren  16347