Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1odm Structured version   Visualization version   GIF version

Theorem f1odm 6098
 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
StepHypRef Expression
1 f1ofn 6095 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 5948 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480  dom cdm 5074   Fn wfn 5842  –1-1-onto→wf1o 5846 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 197  df-an 386  df-fn 5850  df-f 5851  df-f1 5852  df-f1o 5854 This theorem is referenced by:  f1imacnv  6110  f1opw2  6841  xpcomco  7994  domss2  8063  mapen  8068  ssenen  8078  phplem4  8086  php3  8090  f1opwfi  8214  unxpwdom2  8437  cnfcomlem  8540  ackbij2lem2  9006  ackbij2lem3  9007  fin4en1  9075  enfin2i  9087  hashfacen  13176  gsumpropd2lem  17194  symgbas  17721  symgfixf1  17778  f1omvdmvd  17784  f1omvdconj  17787  pmtrfb  17806  symggen  17811  symggen2  17812  psgnunilem1  17834  basqtop  21424  reghmph  21506  nrmhmph  21507  indishmph  21511  ordthmeolem  21514  ufldom  21676  tgpconncompeqg  21825  imasf1oxms  22204  icchmeo  22648  dvcvx  23687  dvloglem  24294  f1ocnt  29397  madjusmdetlem2  29673  madjusmdetlem4  29675  tpr2rico  29737  ballotlemrv  30359  subfacp1lem2b  30868  subfacp1lem5  30871  poimirlem3  33041  ismtyres  33236  eldioph2lem1  36800  lnmlmic  37135  ntrclsiex  37830  ntrneiiex  37853  ssnnf1octb  38853
 Copyright terms: Public domain W3C validator