Theorem fdm 5433

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

Syntax hints:   -> wi 4   = wceq 1373   dom cdm 4676   Fn wfn 5267   -->wf 5268

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 5275  df-f 5276

This theorem is referenced by:  fdmd  5434  fdmi  5435  fssxp  5445  ffdm  5448  dmfex  5467  f00  5469  f0dom0  5471  f0rn0  5472  foima  5505  fimadmfo  5509  foco  5511  resdif  5546  fimacnv  5711  dff3im  5727  ffvresb  5745  resflem  5746  fmptco  5748  focdmex  6202  issmo2  6377  smoiso  6390  tfrcllemubacc  6447  rdgon  6474  frecabcl  6487  frecsuclem  6494  mapprc  6741  elpm2r  6755  map0b  6776  mapsn  6779  brdomg  6839  pw2f1odclem  6933  fopwdom  6935  casef  7192  nn0supp  9349  frecuzrdgdomlem  10564  frecuzrdgsuctlem  10570  zfz1isolemiso  10986  ennnfonelemex  12818  intopsn  13232  iscnp3  14708  cnpnei  14724  cnntr  14730  cncnp  14735  cndis  14746  psmetdmdm  14829  xmetres  14887  metres  14888  metcnp  15017  dvcj  15214  nninfall  15983