Theorem fdm 5488

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

Syntax hints:   -> wi 4   = wceq 1397   dom cdm 4725   Fn wfn 5321   -->wf 5322

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 5329  df-f 5330

This theorem is referenced by:  fdmd  5489  fdmi  5490  fssxp  5502  ffdm  5505  dmfex  5526  f00  5528  f0dom0  5530  f0rn0  5531  foima  5564  fimadmfo  5568  foco  5570  resdif  5605  fimacnv  5776  dff3im  5792  ffvresb  5810  resflem  5811  fmptco  5813  focdmex  6277  issmo2  6455  smoiso  6468  tfrcllemubacc  6525  rdgon  6552  frecabcl  6565  frecsuclem  6572  mapprc  6821  elpm2r  6835  map0b  6856  mapsn  6859  brdomg  6919  pw2f1odclem  7020  fopwdom  7022  casef  7287  nn0supp  9454  frecuzrdgdomlem  10680  frecuzrdgsuctlem  10686  zfz1isolemiso  11104  ennnfonelemex  13053  intopsn  13468  iscnp3  14946  cnpnei  14962  cnntr  14968  cncnp  14973  cndis  14984  psmetdmdm  15067  xmetres  15125  metres  15126  metcnp  15255  dvcj  15452  wlkm  16209  upgr2wlkdc  16247  wlkres  16249  nninfall  16662