Theorem fdm 5479

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

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719   Fn wfn 5313   -->wf 5314

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 5321  df-f 5322

This theorem is referenced by:  fdmd  5480  fdmi  5481  fssxp  5493  ffdm  5496  dmfex  5517  f00  5519  f0dom0  5521  f0rn0  5522  foima  5555  fimadmfo  5559  foco  5561  resdif  5596  fimacnv  5766  dff3im  5782  ffvresb  5800  resflem  5801  fmptco  5803  focdmex  6266  issmo2  6441  smoiso  6454  tfrcllemubacc  6511  rdgon  6538  frecabcl  6551  frecsuclem  6558  mapprc  6807  elpm2r  6821  map0b  6842  mapsn  6845  brdomg  6905  pw2f1odclem  7003  fopwdom  7005  casef  7266  nn0supp  9432  frecuzrdgdomlem  10651  frecuzrdgsuctlem  10657  zfz1isolemiso  11074  ennnfonelemex  13001  intopsn  13416  iscnp3  14893  cnpnei  14909  cnntr  14915  cncnp  14920  cndis  14931  psmetdmdm  15014  xmetres  15072  metres  15073  metcnp  15202  dvcj  15399  wlkm  16085  upgr2wlkdc  16121  wlkres  16123  nninfall  16463