Theorem fdm 5227

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 5224	. 2 ⊢ (F:A–→B → F Fn A)
2		fndm 5183	. 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 4773   Fn wfn 4777  –→wf 4778

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

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

This theorem is referenced by:  fdmi  5228  fssxp  5233  ffdm  5235  dmfex  5248  f00  5250  foima  5275  foco  5280  f1ores  5301  f1imacnv  5303  resdif  5307  fimacnv  5412  dff3  5421  dffo4  5424  ffvresb  5432  mapprc  6005  map0b  6025  mapsn  6027  enprmaplem3  6079  enprmaplem6  6082