Theorem fdm 5166

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 5161	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5113	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1289   dom cdm 4438   Fn wfn 5010   -->wf 5011

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 5018  df-f 5019

This theorem is referenced by:  fdmd  5167  fdmi  5168  fssxp  5178  ffdm  5181  dmfex  5200  f00  5202  f0dom0  5204  f0rn0  5205  foima  5238  foco  5243  resdif  5275  fimacnv  5428  dff3im  5444  ffvresb  5461  resflem  5462  fmptco  5464  fornex  5886  issmo2  6054  smoiso  6067  tfrcllemubacc  6124  rdgon  6151  frecabcl  6164  frecsuclem  6171  mapprc  6409  elpm2r  6423  map0b  6444  mapsn  6447  brdomg  6465  fopwdom  6552  casef  6779  nn0supp  8725  frecuzrdgdomlem  9824  frecuzrdgsuctlem  9830  zfz1isolemiso  10244  nninfall  11900