Theorem fdmd 5480

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

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719   -->wf 5314

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 5321  df-f 5322

This theorem is referenced by:  fssdmd  5487  fssdm  5488  ctssdccl  7278  wrddm  11079  swrdclg  11182  cats1un  11253  s2dmg  11322  1arith  12890  ennnfonelemg  12974  ennnfonelemrnh  12987  ennnfonelemf1  12989  ctinfomlemom  12998  ctinf  13001  igsumval  13423  ghmrn  13794  psrbaglesuppg  14636  psrbagfi  14637  lmbrf  14889  cnntri  14898  cncnp  14904  lmtopcnp  14924  txcnp  14945  hmeores  14989  xmetdmdm  15030  metn0  15052  ellimc3apf  15334  limccnpcntop  15349  dvfvalap  15355  dvcjbr  15382  dvcj  15383  dvfre  15384  dvexp  15385  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  wrdupgren  15896  wrdumgren  15906