Theorem fdmd 5479

Description: Deduction form of fdm 5478. 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 5478	. 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 4718   -->wf 5313

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

This theorem is referenced by:  fssdmd  5486  fssdm  5487  ctssdccl  7274  wrddm  11074  swrdclg  11177  cats1un  11248  s2dmg  11317  1arith  12885  ennnfonelemg  12969  ennnfonelemrnh  12982  ennnfonelemf1  12984  ctinfomlemom  12993  ctinf  12996  igsumval  13418  ghmrn  13789  psrbaglesuppg  14630  psrbagfi  14631  lmbrf  14883  cnntri  14892  cncnp  14898  lmtopcnp  14918  txcnp  14939  hmeores  14983  xmetdmdm  15024  metn0  15046  ellimc3apf  15328  limccnpcntop  15343  dvfvalap  15349  dvcjbr  15376  dvcj  15377  dvfre  15378  dvexp  15379  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  wrdupgren  15890  wrdumgren  15900