Theorem fdmd 5496

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4731   -->wf 5329

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 5336  df-f 5337

This theorem is referenced by:  fssdmd  5503  fssdm  5504  suppsnopdc  6428  ctssdccl  7353  wrddm  11170  swrdclg  11280  cats1un  11351  s2dmg  11420  1arith  13003  ennnfonelemg  13087  ennnfonelemrnh  13100  ennnfonelemf1  13102  ctinfomlemom  13111  ctinf  13114  igsumval  13536  ghmrn  13907  psrbaglesuppg  14751  psrbagfi  14753  lmbrf  15009  cnntri  15018  cncnp  15024  lmtopcnp  15044  txcnp  15065  hmeores  15109  xmetdmdm  15150  metn0  15172  ellimc3apf  15454  limccnpcntop  15469  dvfvalap  15475  dvcjbr  15502  dvcj  15503  dvfre  15504  dvexp  15505  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  wrdupgren  16020  wrdumgren  16030  gfsumval  16792