Theorem f1odm 6831

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 6828	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6647	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

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

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 6546  df-f 6547  df-f1 6548  df-f1o 6550

This theorem is used by:  f1imacnv  6844  f1ounsn  7281  f1opw2  7678  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  18766  symgfixf1  19538  f1omvdmvd  19544  f1omvdconj  19547  pmtrfb  19566  symggen  19571  symggen2  19572  psgnunilem1  19594  basqtop  23905  reghmph  23987  nrmhmph  23988  indishmph  23992  ordthmeolem  23995  ufldom  24156  tgpconncompeqg  24306  imasf1oxms  24683  icchmeo  25137  dvcvx  26216  dvloglem  26850  f1ocnt  33182  cycpmconjvlem  33492  cycpmconjslem2  33506  madjusmdetlem2  34249  madjusmdetlem4  34251  tpr2rico  34333  ballotlemrv  34942  reprpmtf1o  35045  hgt750lemg  35073  vonf1owevOLD  35618  subfacp1lem2b  35694  subfacp1lem5  35697  poimirlem3  38315  ismtyres  38500  eldioph2lem1  43532  lnmlmic  43856  ntrclsiex  44820  ntrneiiex  44843  ssnnf1octb  45953  f1oresf1o  48068  grimuhgr  48693  isubgr3stgrlem3  48774