Theorem fdm 5050

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5046	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 4998	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1243  dom cdm 4345   Fn wfn 4897  ⟶wf 4898

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

This theorem depends on definitions:  df-bi 110  df-fn 4905  df-f 4906

This theorem is referenced by:  fdmi  5051  fssxp  5058  ffdm  5061  dmfex  5079  f00  5081  foima  5111  foco  5116  resdif  5148  fimacnv  5296  dff3im  5312  ffvresb  5328  fmptco  5330  fornex  5742  issmo2  5904  smoiso  5917  brdomg  6229  fopwdom  6310  nn0supp  8234