Theorem fdmd 5486

Description: Deduction form of fdm 5485. 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 5485	. 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 4723   -->wf 5320

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 5327  df-f 5328

This theorem is referenced by:  fssdmd  5493  fssdm  5494  ctssdccl  7301  wrddm  11111  swrdclg  11221  cats1un  11292  s2dmg  11361  1arith  12930  ennnfonelemg  13014  ennnfonelemrnh  13027  ennnfonelemf1  13029  ctinfomlemom  13038  ctinf  13041  igsumval  13463  ghmrn  13834  psrbaglesuppg  14676  psrbagfi  14677  lmbrf  14929  cnntri  14938  cncnp  14944  lmtopcnp  14964  txcnp  14985  hmeores  15029  xmetdmdm  15070  metn0  15092  ellimc3apf  15374  limccnpcntop  15389  dvfvalap  15395  dvcjbr  15422  dvcj  15423  dvfre  15424  dvexp  15425  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  wrdupgren  15937  wrdumgren  15947