Theorem f1odm 6767

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5616   Fn wfn 6476  –1-1-onto→wf1o 6480

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 6484  df-f 6485  df-f1 6486  df-f1o 6488

This theorem is referenced by:  f1imacnv  6779  f1ounsn  7206  f1opw2  7601  xpcomco  8980  domss2  9049  mapen  9054  ssenen  9064  phplem2  9114  php3  9118  f1opwfi  9240  unxpwdom2  9474  cnfcomlem  9589  djuun  9819  ackbij2lem2  10130  ackbij2lem3  10131  fin4en1  10200  enfin2i  10212  gsumpropd2lem  18587  symgfixf1  19350  f1omvdmvd  19356  f1omvdconj  19359  pmtrfb  19378  symggen  19383  symggen2  19384  psgnunilem1  19406  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  32780  cycpmconjvlem  33108  cycpmconjslem2  33122  madjusmdetlem2  33839  madjusmdetlem4  33841  tpr2rico  33923  ballotlemrv  34531  reprpmtf1o  34637  hgt750lemg  34665  vonf1owev  35150  subfacp1lem2b  35223  subfacp1lem5  35226  poimirlem3  37669  ismtyres  37854  eldioph2lem1  42799  lnmlmic  43127  ntrclsiex  44092  ntrneiiex  44115  ssnnf1octb  45237  f1oresf1o  47327  grimuhgr  47924  isubgr3stgrlem3  48005