Theorem fdm 5226

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

Assertion

Ref	Expression
fdm	⊢ (F:A–→B → dom F = A)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5223	. 2 ⊢ (F:A–→B → F Fn A)
2		fndm 5182	. 2 ⊢ (F Fn A → dom F = A)
3	1, 2	syl 15	1 ⊢ (F:A–→B → dom F = A)

Syntax hints:   → wi 4   = wceq 1642  dom cdm 4772   Fn wfn 4776  –→wf 4777

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 4790  df-f 4791

This theorem is referenced by:  fdmi  5227  fssxp  5232  ffdm  5234  dmfex  5247  f00  5249  foima  5274  foco  5279  f1ores  5300  f1imacnv  5302  resdif  5306  fimacnv  5411  dff3  5420  dffo4  5423  ffvresb  5431  mapprc  6004  map0b  6024  mapsn  6026  enprmaplem3  6078  enprmaplem6  6081