Theorem fdm 5363

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

Syntax hints:   -> wi 4   = wceq 1353   dom cdm 4620   Fn wfn 5203   -->wf 5204

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 5211  df-f 5212

This theorem is referenced by:  fdmd  5364  fdmi  5365  fssxp  5375  ffdm  5378  dmfex  5397  f00  5399  f0dom0  5401  f0rn0  5402  foima  5435  foco  5440  resdif  5475  fimacnv  5637  dff3im  5653  ffvresb  5671  resflem  5672  fmptco  5674  focdmex  6106  issmo2  6280  smoiso  6293  tfrcllemubacc  6350  rdgon  6377  frecabcl  6390  frecsuclem  6397  mapprc  6642  elpm2r  6656  map0b  6677  mapsn  6680  brdomg  6738  fopwdom  6826  casef  7077  nn0supp  9201  frecuzrdgdomlem  10387  frecuzrdgsuctlem  10393  zfz1isolemiso  10787  ennnfonelemex  12382  intopsn  12652  iscnp3  13274  cnpnei  13290  cnntr  13296  cncnp  13301  cndis  13312  psmetdmdm  13395  xmetres  13453  metres  13454  metcnp  13583  dvcj  13744  nninfall  14319