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  ctssdccl  7457  hashf1lem1  11307  wrddm  11334  swrdclg  11444  cats1un  11515  s2dmg  11584  1arith  13175  ennnfonelemg  13352  ennnfonelemrnh  13365  ennnfonelemf1  13367  ctinfomlemom  13376  ctinf  13379  gzsumval  13769  ghmrn  14119  cntzmhm2  14174  gsumvalfi  14242  gsumresfi  14263  gsum2dfilem2  14272  psrbaglesuppg  15166  psrbagfi  15168  lmbrf  15441  cnntri  15450  cncnp  15456  lmtopcnp  15476  txcnp  15497  hmeores  15541  xmetdmdm  15582  metn0  15604  ellimc3apf  15886  limccnpcntop  15901  dvfvalap  15907  dvcjbr  15934  dvcj  15935  dvfre  15936  dvexp  15937  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  wrdupgren  16542  wrdumgren  16552