Theorem f1odm 5810

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 5807	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5670	. 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 1383   dom cdm 4989   Fn wfn 5573   -1-1-onto->wf1o 5577

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 371  df-fn 5581  df-f 5582  df-f1 5583  df-f1o 5585

This theorem is referenced by:  f1imacnv  5822  f1opw2  6513  xpcomco  7609  domss2  7678  mapen  7683  ssenen  7693  phplem4  7701  php3  7705  f1opwfi  7826  unxpwdom2  8017  cnfcomlem  8146  cnfcomlemOLD  8154  ackbij2lem2  8623  ackbij2lem3  8624  fin4en1  8692  enfin2i  8704  hashfacen  12485  gsumpropd2lem  15879  symgbas  16384  symgfixf1  16441  f1omvdmvd  16447  f1omvdconj  16450  pmtrfb  16469  symggen  16474  symggen2  16475  psgnunilem1  16497  basqtop  20190  reghmph  20272  nrmhmph  20273  indishmph  20277  ordthmeolem  20280  ufldom  20441  tgpconcompeqg  20588  imasf1oxms  20970  icchmeo  21419  dvcvx  22399  dvloglem  23007  tpr2rico  27872  ballotlemrv  28436  subfacp1lem2b  28603  subfacp1lem5  28606  ismtyres  30280  eldioph2lem1  30669  lnmlmic  31010