Theorem fdm 5431

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 5425	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5373	. 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 4675   Fn wfn 5266   -->wf 5267

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

This theorem is referenced by:  fdmd  5432  fdmi  5433  fssxp  5443  ffdm  5446  dmfex  5465  f00  5467  f0dom0  5469  f0rn0  5470  foima  5503  fimadmfo  5507  foco  5509  resdif  5544  fimacnv  5709  dff3im  5725  ffvresb  5743  resflem  5744  fmptco  5746  focdmex  6200  issmo2  6375  smoiso  6388  tfrcllemubacc  6445  rdgon  6472  frecabcl  6485  frecsuclem  6492  mapprc  6739  elpm2r  6753  map0b  6774  mapsn  6777  brdomg  6837  pw2f1odclem  6931  fopwdom  6933  casef  7190  nn0supp  9347  frecuzrdgdomlem  10562  frecuzrdgsuctlem  10568  zfz1isolemiso  10984  ennnfonelemex  12785  intopsn  13199  iscnp3  14675  cnpnei  14691  cnntr  14697  cncnp  14702  cndis  14713  psmetdmdm  14796  xmetres  14854  metres  14855  metcnp  14984  dvcj  15181  nninfall  15950