Theorem fdm 5368

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 5362	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5312	. 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 4624   Fn wfn 5208   -->wf 5209

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 5216  df-f 5217

This theorem is referenced by:  fdmd  5369  fdmi  5370  fssxp  5380  ffdm  5383  dmfex  5402  f00  5404  f0dom0  5406  f0rn0  5407  foima  5440  foco  5445  resdif  5480  fimacnv  5642  dff3im  5658  ffvresb  5676  resflem  5677  fmptco  5679  focdmex  6111  issmo2  6285  smoiso  6298  tfrcllemubacc  6355  rdgon  6382  frecabcl  6395  frecsuclem  6402  mapprc  6647  elpm2r  6661  map0b  6682  mapsn  6685  brdomg  6743  fopwdom  6831  casef  7082  nn0supp  9222  frecuzrdgdomlem  10410  frecuzrdgsuctlem  10416  zfz1isolemiso  10810  ennnfonelemex  12405  intopsn  12716  iscnp3  13485  cnpnei  13501  cnntr  13507  cncnp  13512  cndis  13523  psmetdmdm  13606  xmetres  13664  metres  13665  metcnp  13794  dvcj  13955  nninfall  14529