Theorem fdmd 5540

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   dom cdm 4774   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fssdmd  5548  fssdm  5549  suppsnopdc  6490  ctssdccl  7452  hashf1lem1  11301  wrddm  11328  swrdclg  11438  cats1un  11509  s2dmg  11578  1arith  13169  ennnfonelemg  13346  ennnfonelemrnh  13359  ennnfonelemf1  13361  ctinfomlemom  13370  ctinf  13373  gzsumval  13763  ghmrn  14113  cntzmhm2  14168  gsumvalfi  14236  psrbaglesuppg  15141  psrbagfi  15143  lmbrf  15407  cnntri  15416  cncnp  15422  lmtopcnp  15442  txcnp  15463  hmeores  15507  xmetdmdm  15548  metn0  15570  ellimc3apf  15852  limccnpcntop  15867  dvfvalap  15873  dvcjbr  15900  dvcj  15901  dvfre  15902  dvexp  15903  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  wrdupgren  16503  wrdumgren  16513