Theorem f1odm 6820

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

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

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 6534  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is used by:  f1imacnv  6833  f1ounsn  7272  f1opw2  7668  xpcomco  9070  domss2  9139  mapen  9144  ssenen  9154  phplem2  9204  php3  9208  f1opwfi  9329  unxpwdom2  9566  cnfcomlem  9684  djuun  9988  ackbij2lem2  10298  ackbij2lem3  10299  fin4en1  10368  enfin2i  10380  gsumpropd2lem  18848  symgfixf1  19631  f1omvdmvd  19637  f1omvdconj  19640  pmtrfb  19659  symggen  19664  symggen2  19665  psgnunilem1  19687  basqtop  24010  reghmph  24092  nrmhmph  24093  indishmph  24097  ordthmeolem  24100  ufldom  24261  tgpconncompeqg  24411  imasf1oxms  24788  icchmeo  25242  dvcvx  26320  dvloglem  26958  f1ocnt  33374  cycpmconjvlem  33684  cycpmconjslem2  33698  madjusmdetlem2  34442  madjusmdetlem4  34444  tpr2rico  34526  ballotlemrv  35135  reprpmtf1o  35238  hgt750lemg  35266  vonf1owevOLD  35862  subfacp1lem2b  35915  subfacp1lem5  35918  poimirlem3  38509  ismtyres  38710  eldioph2lem1  43724  lnmlmic  44048  ntrclsiex  45012  ntrneiiex  45035  ssnnf1octb  46152  f1oresf1o  48304  grimuhgr  48929  isubgr3stgrlem3  49010