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

Theorem f1odm 6179
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 6176 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 6028 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  dom cdm 5143   Fn wfn 5921  1-1-ontowf1o 5925
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 385  df-fn 5929  df-f 5930  df-f1 5931  df-f1o 5933
This theorem is referenced by:  f1imacnv  6191  f1opw2  6930  xpcomco  8091  domss2  8160  mapen  8165  ssenen  8175  phplem4  8183  php3  8187  f1opwfi  8311  unxpwdom2  8534  cnfcomlem  8634  ackbij2lem2  9100  ackbij2lem3  9101  fin4en1  9169  enfin2i  9181  hashfacen  13276  gsumpropd2lem  17320  symgbas  17846  symgfixf1  17903  f1omvdmvd  17909  f1omvdconj  17912  pmtrfb  17931  symggen  17936  symggen2  17937  psgnunilem1  17959  basqtop  21562  reghmph  21644  nrmhmph  21645  indishmph  21649  ordthmeolem  21652  ufldom  21813  tgpconncompeqg  21962  imasf1oxms  22341  icchmeo  22787  dvcvx  23828  dvloglem  24439  f1ocnt  29687  madjusmdetlem2  30022  madjusmdetlem4  30024  tpr2rico  30086  ballotlemrv  30709  reprpmtf1o  30832  hgt750lemg  30860  subfacp1lem2b  31289  subfacp1lem5  31292  poimirlem3  33542  ismtyres  33737  eldioph2lem1  37640  lnmlmic  37975  ntrclsiex  38668  ntrneiiex  38691  ssnnf1octb  39696
  Copyright terms: Public domain W3C validator