Theorem fdm 5387

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

Syntax hints:   -> wi 4   = wceq 1364   dom cdm 4641   Fn wfn 5227   -->wf 5228

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 5235  df-f 5236

This theorem is referenced by:  fdmd  5388  fdmi  5389  fssxp  5399  ffdm  5402  dmfex  5421  f00  5423  f0dom0  5425  f0rn0  5426  foima  5459  foco  5464  resdif  5499  fimacnv  5662  dff3im  5678  ffvresb  5696  resflem  5697  fmptco  5699  focdmex  6135  issmo2  6309  smoiso  6322  tfrcllemubacc  6379  rdgon  6406  frecabcl  6419  frecsuclem  6426  mapprc  6673  elpm2r  6687  map0b  6708  mapsn  6711  brdomg  6769  pw2f1odclem  6857  fopwdom  6859  casef  7112  nn0supp  9253  frecuzrdgdomlem  10443  frecuzrdgsuctlem  10449  zfz1isolemiso  10846  ennnfonelemex  12460  intopsn  12836  iscnp3  14140  cnpnei  14156  cnntr  14162  cncnp  14167  cndis  14178  psmetdmdm  14261  xmetres  14319  metres  14320  metcnp  14449  dvcj  14610  nninfall  15196