Theorem fdmd 5535

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

Syntax hints:   -> wi 4   = wceq 1402   dom cdm 4769   -->wf 5368

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 5375  df-f 5376

This theorem is referenced by:  fssdmd  5543  fssdm  5544  suppsnopdc  6480  ctssdccl  7441  hashf1lem1  11263  wrddm  11290  swrdclg  11400  cats1un  11471  s2dmg  11540  1arith  13124  ennnfonelemg  13272  ennnfonelemrnh  13285  ennnfonelemf1  13287  ctinfomlemom  13296  ctinf  13299  gzsumval  13687  ghmrn  14037  gsumvalfi  14129  psrbaglesuppg  14980  psrbagfi  14982  lmbrf  15239  cnntri  15248  cncnp  15254  lmtopcnp  15274  txcnp  15295  hmeores  15339  xmetdmdm  15380  metn0  15402  ellimc3apf  15684  limccnpcntop  15699  dvfvalap  15705  dvcjbr  15732  dvcj  15733  dvfre  15734  dvexp  15735  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  wrdupgren  16251  wrdumgren  16261