Theorem f1odm 6807

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

Assertion

Ref	Expression
f1odm	⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 6804	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6624	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641   Fn wfn 6509  –1-1-onto→wf1o 6513

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 207  df-an 396  df-fn 6517  df-f 6518  df-f1 6519  df-f1o 6521

This theorem is referenced by:  f1imacnv  6819  f1ounsn  7250  f1opw2  7647  xpcomco  9036  domss2  9106  mapen  9111  ssenen  9121  phplem2  9175  php3  9179  f1opwfi  9314  unxpwdom2  9548  cnfcomlem  9659  djuun  9886  ackbij2lem2  10199  ackbij2lem3  10200  fin4en1  10269  enfin2i  10281  gsumpropd2lem  18613  symgfixf1  19374  f1omvdmvd  19380  f1omvdconj  19383  pmtrfb  19402  symggen  19407  symggen2  19408  psgnunilem1  19430  basqtop  23605  reghmph  23687  nrmhmph  23688  indishmph  23692  ordthmeolem  23695  ufldom  23856  tgpconncompeqg  24006  imasf1oxms  24384  icchmeo  24845  icchmeoOLD  24846  dvcvx  25932  dvloglem  26564  f1ocnt  32732  cycpmconjvlem  33105  cycpmconjslem2  33119  madjusmdetlem2  33825  madjusmdetlem4  33827  tpr2rico  33909  ballotlemrv  34518  reprpmtf1o  34624  hgt750lemg  34652  vonf1owev  35102  subfacp1lem2b  35175  subfacp1lem5  35178  poimirlem3  37624  ismtyres  37809  eldioph2lem1  42755  lnmlmic  43084  ntrclsiex  44049  ntrneiiex  44072  ssnnf1octb  45195  f1oresf1o  47295  grimuhgr  47891  isubgr3stgrlem3  47971