Theorem f1odm 6850

Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

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

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 6847	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6666	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  ⟶1-1ontowf1o 6557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6561  df-f 6562  df-f1 6563  df-f1o 6565

This theorem is used by:  f1imacnv  6863  f1ounsn  7303  f1opw2  7700  xpcomco  9114  domss2  9183  mapen  9188  ssenen  9198  phplem2  9248  php3  9252  f1opwfi  9373  unxpwdom2  9609  cnfcomlem  9727  djuun  10034  ackbij2lem2  10344  ackbij2lem3  10345  fin4en1  10414  enfin2i  10426  gsumpropd2lem  18897  symgfixf1  19681  f1omvdmvd  19687  f1omvdconj  19690  pmtrfb  19709  symggen  19714  symggen2  19715  psgnunilem1  19737  basqtop  24060  reghmph  24142  nrmhmph  24143  indishmph  24147  ordthmeolem  24150  ufldom  24311  tgpconncompeqg  24461  imasf1oxms  24838  icchmeo  25292  dvcvx  26370  dvloglem  27006  f1ocnt  33462  cycpmconjvlem  33772  cycpmconjslem2  33786  madjusmdetlem2  34530  madjusmdetlem4  34532  tpr2rico  34614  ballotlemrv  35222  reprpmtf1o  35325  hgt750lemg  35353  vonf1owevOLD  36038  subfacp1lem2b  36113  subfacp1lem5  36116  poimirlem3  38733  ismtyres  38934  eldioph2lem1  43964  lnmlmic  44283  ntrclsiex  45245  ntrneiiex  45268  ssnnf1octb  46414  f1oresf1o  48565  grimuhgr  49190  isubgr3stgrlem3  49271