Theorem fdm 5451

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 5445	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5392	. 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 4693   Fn wfn 5285   -->wf 5286

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 5293  df-f 5294

This theorem is referenced by:  fdmd  5452  fdmi  5453  fssxp  5463  ffdm  5466  dmfex  5487  f00  5489  f0dom0  5491  f0rn0  5492  foima  5525  fimadmfo  5529  foco  5531  resdif  5566  fimacnv  5732  dff3im  5748  ffvresb  5766  resflem  5767  fmptco  5769  focdmex  6223  issmo2  6398  smoiso  6411  tfrcllemubacc  6468  rdgon  6495  frecabcl  6508  frecsuclem  6515  mapprc  6762  elpm2r  6776  map0b  6797  mapsn  6800  brdomg  6860  pw2f1odclem  6956  fopwdom  6958  casef  7216  nn0supp  9382  frecuzrdgdomlem  10599  frecuzrdgsuctlem  10605  zfz1isolemiso  11021  ennnfonelemex  12900  intopsn  13314  iscnp3  14790  cnpnei  14806  cnntr  14812  cncnp  14817  cndis  14828  psmetdmdm  14911  xmetres  14969  metres  14970  metcnp  15099  dvcj  15296  nninfall  16148