Theorem f1odm 6828

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650  –1-1-onto→wf1o 6537

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

This theorem is used by:  f1imacnv  6841  f1ounsn  7280  f1opw2  7676  xpcomco  9089  domss2  9158  mapen  9163  ssenen  9173  phplem2  9223  php3  9227  f1opwfi  9348  unxpwdom2  9585  cnfcomlem  9703  djuun  10010  ackbij2lem2  10320  ackbij2lem3  10321  fin4en1  10390  enfin2i  10402  gsumpropd2lem  18873  symgfixf1  19656  f1omvdmvd  19662  f1omvdconj  19665  pmtrfb  19684  symggen  19689  symggen2  19690  psgnunilem1  19712  basqtop  24035  reghmph  24117  nrmhmph  24118  indishmph  24122  ordthmeolem  24125  ufldom  24286  tgpconncompeqg  24436  imasf1oxms  24813  icchmeo  25267  dvcvx  26345  dvloglem  26981  f1ocnt  33438  cycpmconjvlem  33748  cycpmconjslem2  33762  madjusmdetlem2  34506  madjusmdetlem4  34508  tpr2rico  34590  ballotlemrv  35198  reprpmtf1o  35301  hgt750lemg  35329  vonf1owevOLD  35957  subfacp1lem2b  36032  subfacp1lem5  36035  poimirlem3  38634  ismtyres  38835  eldioph2lem1  43864  lnmlmic  44183  ntrclsiex  45146  ntrneiiex  45169  ssnnf1octb  46302  f1oresf1o  48453  grimuhgr  49078  isubgr3stgrlem3  49159