Theorem f1odm 6804

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

Syntax hints:   → wi 4   = wceq 1559  dom cdm 5643  –1-1-onto→wf1o 6514

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 209  df-an 400  df-fn 6518  df-f 6519  df-f1 6520  df-f1o 6522

This theorem is referenced by:  f1imacnv  6817  f1ounsn  7250  f1opw2  7645  xpcomco  9032  domss2  9101  mapen  9106  ssenen  9116  phplem2  9166  php3  9170  f1opwfi  9292  unxpwdom2  9529  cnfcomlem  9647  djuun  9877  ackbij2lem2  10188  ackbij2lem3  10189  fin4en1  10259  enfin2i  10271  gsumpropd2lem  18703  symgfixf1  19467  f1omvdmvd  19473  f1omvdconj  19476  pmtrfb  19495  symggen  19500  symggen2  19501  psgnunilem1  19523  basqtop  23758  reghmph  23840  nrmhmph  23841  indishmph  23845  ordthmeolem  23848  ufldom  24009  tgpconncompeqg  24159  imasf1oxms  24536  icchmeo  24990  dvcvx  26069  dvloglem  26700  f1ocnt  32962  cycpmconjvlem  33281  cycpmconjslem2  33295  madjusmdetlem2  34085  madjusmdetlem4  34087  tpr2rico  34169  ballotlemrv  34777  reprpmtf1o  34880  hgt750lemg  34908  vonf1owevOLD  35413  subfacp1lem2b  35491  subfacp1lem5  35494  poimirlem3  38082  ismtyres  38267  eldioph2lem1  43301  lnmlmic  43625  ntrclsiex  44589  ntrneiiex  44612  ssnnf1octb  45732  f1oresf1o  47844  grimuhgr  48469  isubgr3stgrlem3  48550