Theorem fdmd 5515

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4749   -->wf 5348

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 5355  df-f 5356

This theorem is referenced by:  fssdmd  5523  fssdm  5524  suppsnopdc  6450  ctssdccl  7402  wrddm  11232  swrdclg  11342  cats1un  11413  s2dmg  11482  1arith  13065  ennnfonelemg  13154  ennnfonelemrnh  13167  ennnfonelemf1  13169  ctinfomlemom  13178  ctinf  13181  igsumval  13603  ghmrn  13974  psrbaglesuppg  14821  psrbagfi  14823  lmbrf  15080  cnntri  15089  cncnp  15095  lmtopcnp  15115  txcnp  15136  hmeores  15180  xmetdmdm  15221  metn0  15243  ellimc3apf  15525  limccnpcntop  15540  dvfvalap  15546  dvcjbr  15573  dvcj  15574  dvfre  15575  dvexp  15576  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  wrdupgren  16091  wrdumgren  16101  gfsumval  16862