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  7289  wrddm  11092  swrdclg  11197  cats1un  11268  s2dmg  11337  1arith  12905  ennnfonelemg  12989  ennnfonelemrnh  13002  ennnfonelemf1  13004  ctinfomlemom  13013  ctinf  13016  igsumval  13438  ghmrn  13809  psrbaglesuppg  14651  psrbagfi  14652  lmbrf  14904  cnntri  14913  cncnp  14919  lmtopcnp  14939  txcnp  14960  hmeores  15004  xmetdmdm  15045  metn0  15067  ellimc3apf  15349  limccnpcntop  15364  dvfvalap  15370  dvcjbr  15397  dvcj  15398  dvfre  15399  dvexp  15400  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  wrdupgren  15911  wrdumgren  15921