Theorem f1odm 5820

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 5817	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5680	. 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 1379   dom cdm 4999   Fn wfn 5583   -1-1-onto->wf1o 5587

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 5591  df-f 5592  df-f1 5593  df-f1o 5595

This theorem is referenced by:  f1imacnv  5832  f1opw2  6512  xpcomco  7607  domss2  7676  mapen  7681  ssenen  7691  phplem4  7699  php3  7703  f1opwfi  7824  unxpwdom2  8014  cnfcomlem  8143  cnfcomlemOLD  8151  ackbij2lem2  8620  ackbij2lem3  8621  fin4en1  8689  enfin2i  8701  hashfacen  12469  ackbijnn  13603  gsumpropd2lem  15827  symgbas  16210  symgfixf1  16268  f1omvdmvd  16274  f1omvdconj  16277  pmtrfb  16296  symggen  16301  symggen2  16302  psgnunilem1  16324  psgnghm2  18412  basqtop  19975  reghmph  20057  nrmhmph  20058  indishmph  20062  ordthmeolem  20065  ufldom  20226  tgpconcompeqg  20373  imasf1oxms  20755  icchmeo  21204  dvcvx  22184  dvloglem  22785  tpr2rico  27558  ballotlemrv  28126  subfacp1lem2b  28293  subfacp1lem5  28296  ismtyres  29935  eldioph2lem1  30325  lnmlmic  30666