Theorem fdm 5534

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

Syntax hints:   -> wi 4   = wceq 1402   dom cdm 4769   Fn wfn 5367   -->wf 5368

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 5375  df-f 5376

This theorem is referenced by:  fdmd  5535  fdmi  5536  fssxp  5550  ffdm  5553  dmfex  5577  f00  5579  f0dom0  5581  f0rn0  5582  foima  5615  fimadmfo  5619  foco  5621  resdif  5656  fimacnv  5828  dff3im  5844  ffvresb  5862  resflem  5863  fmptco  5865  focdmex  6334  fsuppeq  6477  fsuppeqg  6478  issmo2  6550  smoiso  6563  tfrcllemubacc  6620  rdgon  6647  frecabcl  6660  frecsuclem  6667  mapprc  6916  elpm2r  6930  map0b  6958  mapsnd  6960  mapsn  6962  brdomg  7022  pw2f1odclem  7124  fopwdom  7126  casef  7418  nn0supp  9598  frecuzrdgdomlem  10832  frecuzrdgsuctlem  10838  zfz1isolemiso  11269  ennnfonelemex  13283  intopsn  13664  iscnp3  15227  cnpnei  15243  cnntr  15249  cncnp  15254  cndis  15265  psmetdmdm  15348  xmetres  15406  metres  15407  metcnp  15536  dvcj  15733  wlkm  16494  upgr2wlkdc  16532  wlkres  16534  nninfall  16957