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	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

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

Proof of Theorem fdmd

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

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  11921  ennnfonelemrnh  11934  ennnfonelemf1  11936  ctinfomlemom  11945  ctinf  11948  lmbrf  12389  cnntri  12398  cncnp  12404  lmtopcnp  12424  txcnp  12445  hmeores  12489  xmetdmdm  12530  metn0  12552  ellimc3apf  12803  limccnpcntop  12818  dvfvalap  12824  dvcjbr  12846  dvcj  12847  dvfre  12848  dvexp  12849