Theorem fdmd 5235

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

Syntax hints:   -> wi 4   = wceq 1312   dom cdm 4497   -->wf 5075

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

This theorem depends on definitions:  df-bi 116  df-fn 5082  df-f 5083

This theorem is referenced by:  fssdmd  5242  fssdm  5243  ctssdccl  6946  ennnfonelemg  11755  ennnfonelemrnh  11768  ennnfonelemf1  11770  ctinfomlemom  11779  ctinf  11782  lmbrf  12220  cnntri  12229  cncnp  12235  lmtopcnp  12255  txcnp  12276  xmetdmdm  12339  metn0  12361  ellimc3apf  12579  limccnpcntop  12594  dvfvalap  12599