Theorem fdm 5070

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

Assertion

Ref	Expression
fdm	|- ( F : A --> B -> dom F = A )

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5066	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5018	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1284   dom cdm 4363   Fn wfn 4917   -->wf 4918

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

This theorem depends on definitions:  df-bi 115  df-fn 4925  df-f 4926

This theorem is referenced by:  fdmi  5071  fssxp  5078  ffdm  5081  dmfex  5099  f00  5101  foima  5131  foco  5136  resdif  5168  fimacnv  5317  dff3im  5333  ffvresb  5349  fmptco  5351  fornex  5762  issmo2  5927  smoiso  5940  brdomg  6252  fopwdom  6333  nn0supp  8340