Theorem fdmd 5543

Description: Deduction form of fdm 5542. 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 5542	. 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 4776   -->wf 5376

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 5383  df-f 5384

This theorem is used by:  fssdmd  5551  fssdm  5552  suppsnopdc  6494  funisfsuppdc  7298  fdmfifsupp  7301  ctssdccl  7457  hashf1lem1  11306  wrddm  11333  swrdclg  11443  cats1un  11514  s2dmg  11583  1arith  13174  ennnfonelemg  13351  ennnfonelemrnh  13364  ennnfonelemf1  13366  ctinfomlemom  13375  ctinf  13378  gzsumval  13768  ghmrn  14118  cntzmhm2  14173  gsumvalfi  14241  gsumresfi  14262  gsum2dfilem2  14271  psrbagfi  15166  psrbaglesuppg  15170  mvrclfi  15226  mplsubgfilemcl  15232  mplsubgfileminv  15233  lmbrf  15458  cnntri  15467  cncnp  15473  lmtopcnp  15493  txcnp  15514  hmeores  15558  xmetdmdm  15599  metn0  15621  ellimc3apf  15903  limccnpcntop  15918  dvfvalap  15924  dvcjbr  15951  dvcj  15952  dvfre  15953  dvexp  15954  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  wrdupgren  16559  wrdumgren  16569