Theorem f1odm 6720

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5589   Fn wfn 6428  –1-1-onto→wf1o 6432

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 206  df-an 397  df-fn 6436  df-f 6437  df-f1 6438  df-f1o 6440

This theorem is referenced by:  f1imacnv  6732  f1opw2  7524  xpcomco  8849  domss2  8923  mapen  8928  ssenen  8938  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  f1opwfi  9123  unxpwdom2  9347  cnfcomlem  9457  djuun  9684  ackbij2lem2  9996  ackbij2lem3  9997  fin4en1  10065  enfin2i  10077  hashfacenOLD  14167  gsumpropd2lem  18363  symgfixf1  19045  f1omvdmvd  19051  f1omvdconj  19054  pmtrfb  19073  symggen  19078  symggen2  19079  psgnunilem1  19101  basqtop  22862  reghmph  22944  nrmhmph  22945  indishmph  22949  ordthmeolem  22952  ufldom  23113  tgpconncompeqg  23263  imasf1oxms  23645  icchmeo  24104  dvcvx  25184  dvloglem  25803  f1ocnt  31123  cycpmconjvlem  31408  cycpmconjslem2  31422  madjusmdetlem2  31778  madjusmdetlem4  31780  tpr2rico  31862  ballotlemrv  32486  reprpmtf1o  32606  hgt750lemg  32634  subfacp1lem2b  33143  subfacp1lem5  33146  poimirlem3  35780  ismtyres  35966  eldioph2lem1  40582  lnmlmic  40913  ntrclsiex  41663  ntrneiiex  41686  ssnnf1octb  42733  f1oresf1o  44782