Theorem f1odm 6772

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 6769	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6589	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5619   Fn wfn 6481  –1-1-onto→wf1o 6485

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 6489  df-f 6490  df-f1 6491  df-f1o 6493

This theorem is referenced by:  f1imacnv  6784  f1ounsn  7212  f1opw2  7607  xpcomco  8987  domss2  9056  mapen  9061  ssenen  9071  phplem2  9121  php3  9125  f1opwfi  9247  unxpwdom2  9481  cnfcomlem  9596  djuun  9826  ackbij2lem2  10137  ackbij2lem3  10138  fin4en1  10207  enfin2i  10219  gsumpropd2lem  18589  symgfixf1  19351  f1omvdmvd  19357  f1omvdconj  19360  pmtrfb  19379  symggen  19384  symggen2  19385  psgnunilem1  19407  basqtop  23627  reghmph  23709  nrmhmph  23710  indishmph  23714  ordthmeolem  23717  ufldom  23878  tgpconncompeqg  24028  imasf1oxms  24405  icchmeo  24866  icchmeoOLD  24867  dvcvx  25953  dvloglem  26585  f1ocnt  32787  cycpmconjvlem  33117  cycpmconjslem2  33131  madjusmdetlem2  33862  madjusmdetlem4  33864  tpr2rico  33946  ballotlemrv  34554  reprpmtf1o  34660  hgt750lemg  34688  vonf1owev  35173  subfacp1lem2b  35246  subfacp1lem5  35249  poimirlem3  37684  ismtyres  37869  eldioph2lem1  42878  lnmlmic  43206  ntrclsiex  44171  ntrneiiex  44194  ssnnf1octb  45316  f1oresf1o  47415  grimuhgr  48012  isubgr3stgrlem3  48093