Theorem fdmd 5520

Description: Deduction form of fdm 5519. 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 5519	. 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 4754   -->wf 5353

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 5360  df-f 5361

This theorem is referenced by:  fssdmd  5528  fssdm  5529  suppsnopdc  6463  ctssdccl  7415  wrddm  11257  swrdclg  11367  cats1un  11438  s2dmg  11507  1arith  13090  ennnfonelemg  13238  ennnfonelemrnh  13251  ennnfonelemf1  13253  ctinfomlemom  13262  ctinf  13265  igsumval  13653  ghmrn  14010  gfsumval  14102  psrbaglesuppg  14947  psrbagfi  14949  lmbrf  15206  cnntri  15215  cncnp  15221  lmtopcnp  15241  txcnp  15262  hmeores  15306  xmetdmdm  15347  metn0  15369  ellimc3apf  15651  limccnpcntop  15666  dvfvalap  15672  dvcjbr  15699  dvcj  15700  dvfre  15701  dvexp  15702  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  wrdupgren  16217  wrdumgren  16227