Theorem f1odm 6778

Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1odm	⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 6775	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6595	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624   Fn wfn 6487  –1-1-onto→wf1o 6491

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 207  df-an 396  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1imacnv  6790  f1ounsn  7218  f1opw2  7613  xpcomco  8995  domss2  9064  mapen  9069  ssenen  9079  phplem2  9129  php3  9133  f1opwfi  9256  unxpwdom2  9493  cnfcomlem  9608  djuun  9838  ackbij2lem2  10149  ackbij2lem3  10150  fin4en1  10219  enfin2i  10231  gsumpropd2lem  18604  symgfixf1  19366  f1omvdmvd  19372  f1omvdconj  19375  pmtrfb  19394  symggen  19399  symggen2  19400  psgnunilem1  19422  basqtop  23655  reghmph  23737  nrmhmph  23738  indishmph  23742  ordthmeolem  23745  ufldom  23906  tgpconncompeqg  24056  imasf1oxms  24433  icchmeo  24894  icchmeoOLD  24895  dvcvx  25981  dvloglem  26613  f1ocnt  32880  cycpmconjvlem  33223  cycpmconjslem2  33237  madjusmdetlem2  33985  madjusmdetlem4  33987  tpr2rico  34069  ballotlemrv  34677  reprpmtf1o  34783  hgt750lemg  34811  vonf1owev  35302  subfacp1lem2b  35375  subfacp1lem5  35378  poimirlem3  37824  ismtyres  38009  eldioph2lem1  43002  lnmlmic  43330  ntrclsiex  44294  ntrneiiex  44317  ssnnf1octb  45438  f1oresf1o  47536  grimuhgr  48133  isubgr3stgrlem3  48214