Theorem f1odm 6804

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638   Fn wfn 6506  –1-1-onto→wf1o 6510

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 6514  df-f 6515  df-f1 6516  df-f1o 6518

This theorem is referenced by:  f1imacnv  6816  f1ounsn  7247  f1opw2  7644  xpcomco  9031  domss2  9100  mapen  9105  ssenen  9115  phplem2  9169  php3  9173  f1opwfi  9307  unxpwdom2  9541  cnfcomlem  9652  djuun  9879  ackbij2lem2  10192  ackbij2lem3  10193  fin4en1  10262  enfin2i  10274  gsumpropd2lem  18606  symgfixf1  19367  f1omvdmvd  19373  f1omvdconj  19376  pmtrfb  19395  symggen  19400  symggen2  19401  psgnunilem1  19423  basqtop  23598  reghmph  23680  nrmhmph  23681  indishmph  23685  ordthmeolem  23688  ufldom  23849  tgpconncompeqg  23999  imasf1oxms  24377  icchmeo  24838  icchmeoOLD  24839  dvcvx  25925  dvloglem  26557  f1ocnt  32725  cycpmconjvlem  33098  cycpmconjslem2  33112  madjusmdetlem2  33818  madjusmdetlem4  33820  tpr2rico  33902  ballotlemrv  34511  reprpmtf1o  34617  hgt750lemg  34645  vonf1owev  35095  subfacp1lem2b  35168  subfacp1lem5  35171  poimirlem3  37617  ismtyres  37802  eldioph2lem1  42748  lnmlmic  43077  ntrclsiex  44042  ntrneiiex  44065  ssnnf1octb  45188  f1oresf1o  47291  grimuhgr  47887  isubgr3stgrlem3  47967