Theorem fdm 5278

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

Syntax hints:   -> wi 4   = wceq 1331   dom cdm 4539   Fn wfn 5118   -->wf 5119

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

This theorem depends on definitions:  df-bi 116  df-fn 5126  df-f 5127

This theorem is referenced by:  fdmd  5279  fdmi  5280  fssxp  5290  ffdm  5293  dmfex  5312  f00  5314  f0dom0  5316  f0rn0  5317  foima  5350  foco  5355  resdif  5389  fimacnv  5549  dff3im  5565  ffvresb  5583  resflem  5584  fmptco  5586  fornex  6013  issmo2  6186  smoiso  6199  tfrcllemubacc  6256  rdgon  6283  frecabcl  6296  frecsuclem  6303  mapprc  6546  elpm2r  6560  map0b  6581  mapsn  6584  brdomg  6642  fopwdom  6730  casef  6973  nn0supp  9029  frecuzrdgdomlem  10190  frecuzrdgsuctlem  10196  zfz1isolemiso  10582  ennnfonelemex  11927  iscnp3  12372  cnpnei  12388  cnntr  12394  cncnp  12399  cndis  12410  psmetdmdm  12493  xmetres  12551  metres  12552  metcnp  12681  dvcj  12842  nninfall  13204