Theorem fdm 5119

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

Syntax hints:   -> wi 4   = wceq 1285   dom cdm 4401   Fn wfn 4964   -->wf 4965

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem depends on definitions:  df-bi 115  df-fn 4972  df-f 4973

This theorem is referenced by:  fdmi  5120  fssxp  5127  ffdm  5130  dmfex  5148  f00  5150  f0dom0  5152  f0rn0  5153  foima  5186  foco  5191  resdif  5223  fimacnv  5373  dff3im  5389  ffvresb  5403  resflem  5404  fmptco  5406  fornex  5821  issmo2  5986  smoiso  5999  tfrcllemubacc  6056  rdgon  6083  frecabcl  6096  frecsuclem  6103  mapprc  6339  elpm2r  6353  map0b  6374  mapsn  6377  brdomg  6395  fopwdom  6482  casef  6686  nn0supp  8617  frecuzrdgdomlem  9713  frecuzrdgsuctlem  9719  nninfall  11241