Theorem fdm 5343

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

Syntax hints:   -> wi 4   = wceq 1343   dom cdm 4604   Fn wfn 5183   -->wf 5184

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 5191  df-f 5192

This theorem is referenced by:  fdmd  5344  fdmi  5345  fssxp  5355  ffdm  5358  dmfex  5377  f00  5379  f0dom0  5381  f0rn0  5382  foima  5415  foco  5420  resdif  5454  fimacnv  5614  dff3im  5630  ffvresb  5648  resflem  5649  fmptco  5651  fornex  6083  issmo2  6257  smoiso  6270  tfrcllemubacc  6327  rdgon  6354  frecabcl  6367  frecsuclem  6374  mapprc  6618  elpm2r  6632  map0b  6653  mapsn  6656  brdomg  6714  fopwdom  6802  casef  7053  nn0supp  9166  frecuzrdgdomlem  10352  frecuzrdgsuctlem  10358  zfz1isolemiso  10752  ennnfonelemex  12347  intopsn  12598  iscnp3  12843  cnpnei  12859  cnntr  12865  cncnp  12870  cndis  12881  psmetdmdm  12964  xmetres  13022  metres  13023  metcnp  13152  dvcj  13313  nninfall  13889