Theorem f1odm 5840

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 5837	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5696	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 17	1 |- ( F : A -1-1-onto-> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1454   dom cdm 4852   Fn wfn 5595   -1-1-onto->wf1o 5599

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 190  df-an 377  df-fn 5603  df-f 5604  df-f1 5605  df-f1o 5607

This theorem is referenced by:  f1imacnv  5852  f1opw2  6548  xpcomco  7687  domss2  7756  mapen  7761  ssenen  7771  phplem4  7779  php3  7783  f1opwfi  7903  unxpwdom2  8128  cnfcomlem  8229  ackbij2lem2  8695  ackbij2lem3  8696  fin4en1  8764  enfin2i  8776  hashfacen  12649  gsumpropd2lem  16564  symgbas  17069  symgfixf1  17126  f1omvdmvd  17132  f1omvdconj  17135  pmtrfb  17154  symggen  17159  symggen2  17160  psgnunilem1  17182  basqtop  20774  reghmph  20856  nrmhmph  20857  indishmph  20861  ordthmeolem  20864  ufldom  21025  tgpconcompeqg  21174  imasf1oxms  21552  icchmeo  22017  dvcvx  23020  dvloglem  23641  f1ocnt  28424  madjusmdetlem2  28702  madjusmdetlem4  28704  tpr2rico  28766  ballotlemrv  29400  ballotlemrvOLD  29438  subfacp1lem2b  29952  subfacp1lem5  29955  poimirlem3  31987  ismtyres  32184  eldioph2lem1  35646  lnmlmic  35990  ssnnf1octb  37507