Theorem f1odm 6784

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631   Fn wfn 6493  –1-1-onto→wf1o 6497

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 6501  df-f 6502  df-f1 6503  df-f1o 6505

This theorem is referenced by:  f1imacnv  6796  f1ounsn  7227  f1opw2  7622  xpcomco  9005  domss2  9074  mapen  9079  ssenen  9089  phplem2  9139  php3  9143  f1opwfi  9266  unxpwdom2  9503  cnfcomlem  9620  djuun  9850  ackbij2lem2  10161  ackbij2lem3  10162  fin4en1  10231  enfin2i  10243  gsumpropd2lem  18647  symgfixf1  19412  f1omvdmvd  19418  f1omvdconj  19421  pmtrfb  19440  symggen  19445  symggen2  19446  psgnunilem1  19468  basqtop  23676  reghmph  23758  nrmhmph  23759  indishmph  23763  ordthmeolem  23766  ufldom  23927  tgpconncompeqg  24077  imasf1oxms  24454  icchmeo  24908  dvcvx  25987  dvloglem  26612  f1ocnt  32873  cycpmconjvlem  33202  cycpmconjslem2  33216  madjusmdetlem2  33972  madjusmdetlem4  33974  tpr2rico  34056  ballotlemrv  34664  reprpmtf1o  34770  hgt750lemg  34798  vonf1owev  35290  subfacp1lem2b  35363  subfacp1lem5  35366  poimirlem3  37944  ismtyres  38129  eldioph2lem1  43192  lnmlmic  43516  ntrclsiex  44480  ntrneiiex  44503  ssnnf1octb  45624  f1oresf1o  47738  grimuhgr  48363  isubgr3stgrlem3  48444