Theorem fdmd 5442

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

Syntax hints:   -> wi 4   = wceq 1373   dom cdm 4683   -->wf 5276

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 5283  df-f 5284

This theorem is referenced by:  fssdmd  5449  fssdm  5450  ctssdccl  7228  wrddm  11024  swrdclg  11126  cats1un  11197  1arith  12765  ennnfonelemg  12849  ennnfonelemrnh  12862  ennnfonelemf1  12864  ctinfomlemom  12873  ctinf  12876  igsumval  13297  ghmrn  13668  psrbaglesuppg  14509  psrbagfi  14510  lmbrf  14762  cnntri  14771  cncnp  14777  lmtopcnp  14797  txcnp  14818  hmeores  14862  xmetdmdm  14903  metn0  14925  ellimc3apf  15207  limccnpcntop  15222  dvfvalap  15228  dvcjbr  15255  dvcj  15256  dvfre  15257  dvexp  15258  plyaddlem1  15294  plymullem1  15295  plycoeid3  15304  wrdupgren  15767  wrdumgren  15777