Theorem f1odm 6825

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

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

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 6540  df-f 6541  df-f1 6542  df-f1o 6544

This theorem is used by:  f1imacnv  6838  f1ounsn  7277  f1opw2  7673  xpcomco  9069  domss2  9138  mapen  9143  ssenen  9153  phplem2  9203  php3  9207  f1opwfi  9327  unxpwdom2  9564  cnfcomlem  9682  djuun  9935  ackbij2lem2  10245  ackbij2lem3  10246  fin4en1  10315  enfin2i  10327  gsumpropd2lem  18787  symgfixf1  19570  f1omvdmvd  19576  f1omvdconj  19579  pmtrfb  19598  symggen  19603  symggen2  19604  psgnunilem1  19626  basqtop  23943  reghmph  24025  nrmhmph  24026  indishmph  24030  ordthmeolem  24033  ufldom  24194  tgpconncompeqg  24344  imasf1oxms  24721  icchmeo  25175  dvcvx  26254  dvloglem  26893  f1ocnt  33279  cycpmconjvlem  33589  cycpmconjslem2  33603  madjusmdetlem2  34346  madjusmdetlem4  34348  tpr2rico  34430  ballotlemrv  35039  reprpmtf1o  35142  hgt750lemg  35170  vonf1owevOLD  35715  subfacp1lem2b  35768  subfacp1lem5  35771  poimirlem3  38380  ismtyres  38566  eldioph2lem1  43613  lnmlmic  43937  ntrclsiex  44901  ntrneiiex  44924  ssnnf1octb  46034  f1oresf1o  48186  grimuhgr  48811  isubgr3stgrlem3  48892