Theorem fdmd 5354

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

Syntax hints:   -> wi 4   = wceq 1348   dom cdm 4611   -->wf 5194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5201  df-f 5202

This theorem is referenced by:  fssdmd  5361  fssdm  5362  ctssdccl  7088  1arith  12319  ennnfonelemg  12358  ennnfonelemrnh  12371  ennnfonelemf1  12373  ctinfomlemom  12382  ctinf  12385  lmbrf  13009  cnntri  13018  cncnp  13024  lmtopcnp  13044  txcnp  13065  hmeores  13109  xmetdmdm  13150  metn0  13172  ellimc3apf  13423  limccnpcntop  13438  dvfvalap  13444  dvcjbr  13466  dvcj  13467  dvfre  13468  dvexp  13469