Theorem fdmd 5410

Description: Deduction form of fdm 5409. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
fdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
fdmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fdmd

Step	Hyp	Ref	Expression
1		fdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fdm 5409	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4659  ⟶wf 5250

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 5257  df-f 5258

This theorem is referenced by:  fssdmd  5417  fssdm  5418  ctssdccl  7170  wrddm  10922  1arith  12505  ennnfonelemg  12560  ennnfonelemrnh  12573  ennnfonelemf1  12575  ctinfomlemom  12584  ctinf  12587  igsumval  12973  ghmrn  13327  psrbaglesuppg  14158  lmbrf  14383  cnntri  14392  cncnp  14398  lmtopcnp  14418  txcnp  14439  hmeores  14483  xmetdmdm  14524  metn0  14546  ellimc3apf  14814  limccnpcntop  14829  dvfvalap  14835  dvcjbr  14857  dvcj  14858  dvfre  14859  dvexp  14860  plyaddlem1  14893  plymullem1  14894