Theorem fdmd 5279

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

Syntax hints:   -> wi 4   = wceq 1331   dom cdm 4539   -->wf 5119

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 5126  df-f 5127

This theorem is referenced by:  fssdmd  5286  fssdm  5287  ctssdccl  6996  ennnfonelemg  11916  ennnfonelemrnh  11929  ennnfonelemf1  11931  ctinfomlemom  11940  ctinf  11943  lmbrf  12384  cnntri  12393  cncnp  12399  lmtopcnp  12419  txcnp  12440  hmeores  12484  xmetdmdm  12525  metn0  12547  ellimc3apf  12798  limccnpcntop  12813  dvfvalap  12819  dvcjbr  12841  dvcj  12842  dvfre  12843  dvexp  12844