Theorem fdmd 5411

Description: Deduction form of fdm 5410. 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 5410	. 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 4660   -->wf 5251

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 5258  df-f 5259

This theorem is referenced by:  fssdmd  5418  fssdm  5419  ctssdccl  7172  wrddm  10925  1arith  12508  ennnfonelemg  12563  ennnfonelemrnh  12576  ennnfonelemf1  12578  ctinfomlemom  12587  ctinf  12590  igsumval  12976  ghmrn  13330  psrbaglesuppg  14169  lmbrf  14394  cnntri  14403  cncnp  14409  lmtopcnp  14429  txcnp  14450  hmeores  14494  xmetdmdm  14535  metn0  14557  ellimc3apf  14839  limccnpcntop  14854  dvfvalap  14860  dvcjbr  14887  dvcj  14888  dvfre  14889  dvexp  14890  plyaddlem1  14926  plymullem1  14927