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  11300  wrddm  11327  swrdclg  11437  cats1un  11508  s2dmg  11577  1arith  13168  ennnfonelemg  13345  ennnfonelemrnh  13358  ennnfonelemf1  13360  ctinfomlemom  13369  ctinf  13372  gzsumval  13761  ghmrn  14111  gsumvalfi  14203  psrbaglesuppg  15108  psrbagfi  15110  lmbrf  15368  cnntri  15377  cncnp  15383  lmtopcnp  15403  txcnp  15424  hmeores  15468  xmetdmdm  15509  metn0  15531  ellimc3apf  15813  limccnpcntop  15828  dvfvalap  15834  dvcjbr  15861  dvcj  15862  dvfre  15863  dvexp  15864  plyaddlem1  15900  plymullem1  15901  plycoeid3  15910  wrdupgren  16459  wrdumgren  16469