Theorem f1odm 5802

Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1odm	|- ( F : A -1-1-onto-> B -> dom F = A )

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 5799	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5662	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 16	1 |- ( F : A -1-1-onto-> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4988   Fn wfn 5565   -1-1-onto->wf1o 5569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369  df-fn 5573  df-f 5574  df-f1 5575  df-f1o 5577

This theorem is referenced by:  f1imacnv  5814  f1opw2  6501  xpcomco  7600  domss2  7669  mapen  7674  ssenen  7684  phplem4  7692  php3  7696  f1opwfi  7816  unxpwdom2  8006  cnfcomlem  8134  cnfcomlemOLD  8142  ackbij2lem2  8611  ackbij2lem3  8612  fin4en1  8680  enfin2i  8692  hashfacen  12490  gsumpropd2lem  16102  symgbas  16607  symgfixf1  16664  f1omvdmvd  16670  f1omvdconj  16673  pmtrfb  16692  symggen  16697  symggen2  16698  psgnunilem1  16720  basqtop  20381  reghmph  20463  nrmhmph  20464  indishmph  20468  ordthmeolem  20471  ufldom  20632  tgpconcompeqg  20779  imasf1oxms  21161  icchmeo  21610  dvcvx  22590  dvloglem  23200  tpr2rico  28132  ballotlemrv  28725  subfacp1lem2b  28892  subfacp1lem5  28895  ismtyres  30547  eldioph2lem1  30935  lnmlmic  31276