Theorem fdm 5372

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 5366	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5316	. 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 4627   Fn wfn 5212   -->wf 5213

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 5220  df-f 5221

This theorem is referenced by:  fdmd  5373  fdmi  5374  fssxp  5384  ffdm  5387  dmfex  5406  f00  5408  f0dom0  5410  f0rn0  5411  foima  5444  foco  5449  resdif  5484  fimacnv  5646  dff3im  5662  ffvresb  5680  resflem  5681  fmptco  5683  focdmex  6116  issmo2  6290  smoiso  6303  tfrcllemubacc  6360  rdgon  6387  frecabcl  6400  frecsuclem  6407  mapprc  6652  elpm2r  6666  map0b  6687  mapsn  6690  brdomg  6748  fopwdom  6836  casef  7087  nn0supp  9228  frecuzrdgdomlem  10417  frecuzrdgsuctlem  10423  zfz1isolemiso  10819  ennnfonelemex  12415  intopsn  12786  iscnp3  13706  cnpnei  13722  cnntr  13728  cncnp  13733  cndis  13744  psmetdmdm  13827  xmetres  13885  metres  13886  metcnp  14015  dvcj  14176  nninfall  14761