Theorem fdm 5286

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

Syntax hints:   -> wi 4   = wceq 1332   dom cdm 4547   Fn wfn 5126   -->wf 5127

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

This theorem depends on definitions:  df-bi 116  df-fn 5134  df-f 5135

This theorem is referenced by:  fdmd  5287  fdmi  5288  fssxp  5298  ffdm  5301  dmfex  5320  f00  5322  f0dom0  5324  f0rn0  5325  foima  5358  foco  5363  resdif  5397  fimacnv  5557  dff3im  5573  ffvresb  5591  resflem  5592  fmptco  5594  fornex  6021  issmo2  6194  smoiso  6207  tfrcllemubacc  6264  rdgon  6291  frecabcl  6304  frecsuclem  6311  mapprc  6554  elpm2r  6568  map0b  6589  mapsn  6592  brdomg  6650  fopwdom  6738  casef  6981  nn0supp  9053  frecuzrdgdomlem  10221  frecuzrdgsuctlem  10227  zfz1isolemiso  10614  ennnfonelemex  11963  iscnp3  12411  cnpnei  12427  cnntr  12433  cncnp  12438  cndis  12449  psmetdmdm  12532  xmetres  12590  metres  12591  metcnp  12720  dvcj  12881  nninfall  13379