Theorem f1odm 6771

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 6768	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6588	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5620   Fn wfn 6474  –1-1-onto→wf1o 6478

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 206  df-an 397  df-fn 6482  df-f 6483  df-f1 6484  df-f1o 6486

This theorem is referenced by:  f1imacnv  6783  f1opw2  7586  xpcomco  8927  domss2  9001  mapen  9006  ssenen  9016  phplem2  9073  php3  9077  phplem4OLD  9085  php3OLD  9089  f1opwfi  9221  unxpwdom2  9445  cnfcomlem  9556  djuun  9783  ackbij2lem2  10097  ackbij2lem3  10098  fin4en1  10166  enfin2i  10178  hashfacenOLD  14267  gsumpropd2lem  18460  symgfixf1  19141  f1omvdmvd  19147  f1omvdconj  19150  pmtrfb  19169  symggen  19174  symggen2  19175  psgnunilem1  19197  basqtop  22968  reghmph  23050  nrmhmph  23051  indishmph  23055  ordthmeolem  23058  ufldom  23219  tgpconncompeqg  23369  imasf1oxms  23751  icchmeo  24210  dvcvx  25290  dvloglem  25909  f1ocnt  31410  cycpmconjvlem  31695  cycpmconjslem2  31709  madjusmdetlem2  32076  madjusmdetlem4  32078  tpr2rico  32160  ballotlemrv  32786  reprpmtf1o  32906  hgt750lemg  32934  subfacp1lem2b  33442  subfacp1lem5  33445  poimirlem3  35885  ismtyres  36071  eldioph2lem1  40844  lnmlmic  41176  ntrclsiex  41984  ntrneiiex  42007  ssnnf1octb  43060  f1oresf1o  45133