Theorem f1odm 6814

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

Syntax hints:   → wi 4   = wceq 1563  dom cdm 5651  –1-1-onto→wf1o 6524

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 210  df-an 401  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1imacnv  6827  f1ounsn  7260  f1opw2  7655  xpcomco  9043  domss2  9112  mapen  9117  ssenen  9127  phplem2  9177  php3  9181  f1opwfi  9301  unxpwdom2  9538  cnfcomlem  9656  djuun  9900  ackbij2lem2  10210  ackbij2lem3  10211  fin4en1  10281  enfin2i  10293  gsumpropd2lem  18725  symgfixf1  19495  f1omvdmvd  19501  f1omvdconj  19504  pmtrfb  19523  symggen  19528  symggen2  19529  psgnunilem1  19551  basqtop  23825  reghmph  23907  nrmhmph  23908  indishmph  23912  ordthmeolem  23915  ufldom  24076  tgpconncompeqg  24226  imasf1oxms  24603  icchmeo  25057  dvcvx  26136  dvloglem  26767  f1ocnt  33053  cycpmconjvlem  33369  cycpmconjslem2  33383  madjusmdetlem2  34130  madjusmdetlem4  34132  tpr2rico  34214  ballotlemrv  34822  reprpmtf1o  34925  hgt750lemg  34953  vonf1owevOLD  35460  subfacp1lem2b  35539  subfacp1lem5  35542  poimirlem3  38129  ismtyres  38314  eldioph2lem1  43348  lnmlmic  43672  ntrclsiex  44636  ntrneiiex  44659  ssnnf1octb  45771  f1oresf1o  47883  grimuhgr  48508  isubgr3stgrlem3  48589