Theorem f1odm 6366

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

Syntax hints:   → wi 4   = wceq 1637  dom cdm 5324   Fn wfn 6105  –1-1-onto→wf1o 6109

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 198  df-an 385  df-fn 6113  df-f 6114  df-f1 6115  df-f1o 6117

This theorem is referenced by:  f1imacnv  6378  f1opw2  7127  xpcomco  8298  domss2  8367  mapen  8372  ssenen  8382  phplem4  8390  php3  8394  f1opwfi  8518  unxpwdom2  8741  cnfcomlem  8852  djuun  9044  ackbij2lem2  9356  ackbij2lem3  9357  fin4en1  9425  enfin2i  9437  hashfacen  13474  gsumpropd2lem  17497  symgbas  18020  symgfixf1  18077  f1omvdmvd  18083  f1omvdconj  18086  pmtrfb  18105  symggen  18110  symggen2  18111  psgnunilem1  18133  basqtop  21748  reghmph  21830  nrmhmph  21831  indishmph  21835  ordthmeolem  21838  ufldom  21999  tgpconncompeqg  22148  imasf1oxms  22527  icchmeo  22973  dvcvx  24019  dvloglem  24630  f1ocnt  29908  madjusmdetlem2  30241  madjusmdetlem4  30243  tpr2rico  30305  ballotlemrv  30928  reprpmtf1o  31051  hgt750lemg  31079  subfacp1lem2b  31507  subfacp1lem5  31510  poimirlem3  33743  ismtyres  33936  eldioph2lem1  37842  lnmlmic  38176  ntrclsiex  38868  ntrneiiex  38891  ssnnf1octb  39888  f1oresf1o  41897  f1oresf1o2  41898