Theorem fdmd 5417

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

Syntax hints:   -> wi 4   = wceq 1364   dom cdm 4664   -->wf 5255

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 5262  df-f 5263

This theorem is referenced by:  fssdmd  5424  fssdm  5425  ctssdccl  7186  wrddm  10962  1arith  12563  ennnfonelemg  12647  ennnfonelemrnh  12660  ennnfonelemf1  12662  ctinfomlemom  12671  ctinf  12674  igsumval  13094  ghmrn  13465  psrbaglesuppg  14306  psrbagfi  14307  lmbrf  14559  cnntri  14568  cncnp  14574  lmtopcnp  14594  txcnp  14615  hmeores  14659  xmetdmdm  14700  metn0  14722  ellimc3apf  15004  limccnpcntop  15019  dvfvalap  15025  dvcjbr  15052  dvcj  15053  dvfre  15054  dvexp  15055  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101