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

Theorem f1odm 6479
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 6476 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 6317 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1520  dom cdm 5435   Fn wfn 6212  1-1-ontowf1o 6216
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 208  df-an 397  df-fn 6220  df-f 6221  df-f1 6222  df-f1o 6224
This theorem is referenced by:  f1imacnv  6491  f1opw2  7249  xpcomco  8444  domss2  8513  mapen  8518  ssenen  8528  phplem4  8536  php3  8540  f1opwfi  8664  unxpwdom2  8888  cnfcomlem  8997  djuun  9190  ackbij2lem2  9497  ackbij2lem3  9498  fin4en1  9566  enfin2i  9578  hashfacen  13648  gsumpropd2lem  17700  symgbas  18227  symgfixf1  18284  f1omvdmvd  18290  f1omvdconj  18293  pmtrfb  18312  symggen  18317  symggen2  18318  psgnunilem1  18340  basqtop  21991  reghmph  22073  nrmhmph  22074  indishmph  22078  ordthmeolem  22081  ufldom  22242  tgpconncompeqg  22391  imasf1oxms  22770  icchmeo  23216  dvcvx  24288  dvloglem  24900  f1ocnt  30181  cycpmconjvlem  30383  cycpmconjslem2  30393  madjusmdetlem2  30664  madjusmdetlem4  30666  tpr2rico  30728  ballotlemrv  31350  reprpmtf1o  31470  hgt750lemg  31498  subfacp1lem2b  31992  subfacp1lem5  31995  poimirlem3  34372  ismtyres  34564  eldioph2lem1  38792  lnmlmic  39124  ntrclsiex  39839  ntrneiiex  39862  ssnnf1octb  40949  f1oresf1o  42959
  Copyright terms: Public domain W3C validator