Theorem fdm 5495

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4731   Fn wfn 5328   -->wf 5329

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

This theorem depends on definitions:  df-bi 117  df-fn 5336  df-f 5337

This theorem is referenced by:  fdmd  5496  fdmi  5497  fssxp  5510  ffdm  5513  dmfex  5535  f00  5537  f0dom0  5539  f0rn0  5540  foima  5573  fimadmfo  5577  foco  5579  resdif  5614  fimacnv  5784  dff3im  5800  ffvresb  5818  resflem  5819  fmptco  5821  focdmex  6286  fsuppeq  6425  fsuppeqg  6426  issmo2  6498  smoiso  6511  tfrcllemubacc  6568  rdgon  6595  frecabcl  6608  frecsuclem  6615  mapprc  6864  elpm2r  6878  map0b  6899  mapsn  6902  brdomg  6962  pw2f1odclem  7063  fopwdom  7065  casef  7347  nn0supp  9515  frecuzrdgdomlem  10742  frecuzrdgsuctlem  10748  zfz1isolemiso  11166  ennnfonelemex  13115  intopsn  13530  iscnp3  15014  cnpnei  15030  cnntr  15036  cncnp  15041  cndis  15052  psmetdmdm  15135  xmetres  15193  metres  15194  metcnp  15323  dvcj  15520  wlkm  16280  upgr2wlkdc  16318  wlkres  16320  nninfall  16735