Theorem f1odm 6282

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

Syntax hints:   → wi 4   = wceq 1631  dom cdm 5249   Fn wfn 6026  –1-1-onto→wf1o 6030

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 197  df-an 383  df-fn 6034  df-f 6035  df-f1 6036  df-f1o 6038

This theorem is referenced by:  f1imacnv  6294  f1opw2  7035  xpcomco  8206  domss2  8275  mapen  8280  ssenen  8290  phplem4  8298  php3  8302  f1opwfi  8426  unxpwdom2  8649  cnfcomlem  8760  djuun  8952  ackbij2lem2  9264  ackbij2lem3  9265  fin4en1  9333  enfin2i  9345  hashfacen  13440  gsumpropd2lem  17481  symgbas  18007  symgfixf1  18064  f1omvdmvd  18070  f1omvdconj  18073  pmtrfb  18092  symggen  18097  symggen2  18098  psgnunilem1  18120  basqtop  21735  reghmph  21817  nrmhmph  21818  indishmph  21822  ordthmeolem  21825  ufldom  21986  tgpconncompeqg  22135  imasf1oxms  22514  icchmeo  22960  dvcvx  24003  dvloglem  24615  f1ocnt  29899  madjusmdetlem2  30234  madjusmdetlem4  30236  tpr2rico  30298  ballotlemrv  30921  reprpmtf1o  31044  hgt750lemg  31072  subfacp1lem2b  31501  subfacp1lem5  31504  poimirlem3  33745  ismtyres  33939  eldioph2lem1  37849  lnmlmic  38184  ntrclsiex  38877  ntrneiiex  38900  ssnnf1octb  39902  f1oresf1o  41832  f1oresf1o2  41833