Theorem f1odm 6821

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-1-onto→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 6818	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6637	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  –1-1-onto→wf1o 6532

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 6536  df-f 6537  df-f1 6538  df-f1o 6540

This theorem is used by:  f1imacnv  6834  f1ounsn  7273  f1opw2  7669  xpcomco  9065  domss2  9134  mapen  9139  ssenen  9149  phplem2  9199  php3  9203  f1opwfi  9323  unxpwdom2  9560  cnfcomlem  9678  djuun  9931  ackbij2lem2  10241  ackbij2lem3  10242  fin4en1  10311  enfin2i  10323  gsumpropd2lem  18781  symgfixf1  19564  f1omvdmvd  19570  f1omvdconj  19573  pmtrfb  19592  symggen  19597  symggen2  19598  psgnunilem1  19620  basqtop  23937  reghmph  24019  nrmhmph  24020  indishmph  24024  ordthmeolem  24027  ufldom  24188  tgpconncompeqg  24338  imasf1oxms  24715  icchmeo  25169  dvcvx  26247  dvloglem  26885  f1ocnt  33271  cycpmconjvlem  33581  cycpmconjslem2  33595  madjusmdetlem2  34338  madjusmdetlem4  34340  tpr2rico  34422  ballotlemrv  35031  reprpmtf1o  35134  hgt750lemg  35162  vonf1owevOLD  35707  subfacp1lem2b  35760  subfacp1lem5  35763  poimirlem3  38372  ismtyres  38558  eldioph2lem1  43605  lnmlmic  43929  ntrclsiex  44893  ntrneiiex  44916  ssnnf1octb  46026  f1oresf1o  48178  grimuhgr  48803  isubgr3stgrlem3  48884