Theorem f1odm 6826

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

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5663  –1-1-onto→wf1o 6537

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 6541  df-f 6542  df-f1 6543  df-f1o 6545

This theorem is referenced by:  f1imacnv  6839  f1ounsn  7272  f1opw2  7667  xpcomco  9056  domss2  9125  mapen  9130  ssenen  9140  phplem2  9190  php3  9194  f1opwfi  9314  unxpwdom2  9551  cnfcomlem  9669  djuun  9913  ackbij2lem2  10223  ackbij2lem3  10224  fin4en1  10294  enfin2i  10306  gsumpropd2lem  18738  symgfixf1  19508  f1omvdmvd  19514  f1omvdconj  19517  pmtrfb  19536  symggen  19541  symggen2  19542  psgnunilem1  19564  basqtop  23849  reghmph  23931  nrmhmph  23932  indishmph  23936  ordthmeolem  23939  ufldom  24100  tgpconncompeqg  24250  imasf1oxms  24627  icchmeo  25081  dvcvx  26160  dvloglem  26794  f1ocnt  33126  cycpmconjvlem  33442  cycpmconjslem2  33456  madjusmdetlem2  34199  madjusmdetlem4  34201  tpr2rico  34283  ballotlemrv  34891  reprpmtf1o  34994  hgt750lemg  35022  vonf1owevOLD  35575  subfacp1lem2b  35654  subfacp1lem5  35657  poimirlem3  38255  ismtyres  38440  eldioph2lem1  43474  lnmlmic  43798  ntrclsiex  44762  ntrneiiex  44785  ssnnf1octb  45895  f1oresf1o  48010  grimuhgr  48635  isubgr3stgrlem3  48716