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

Theorem f1odm 6788
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 6785 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 6605 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  dom cdm 5633   Fn wfn 6491  1-1-ontowf1o 6495
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 6499  df-f 6500  df-f1 6501  df-f1o 6503
This theorem is referenced by:  f1imacnv  6800  f1opw2  7607  xpcomco  9005  domss2  9079  mapen  9084  ssenen  9094  phplem2  9151  php3  9155  phplem4OLD  9163  php3OLD  9167  f1opwfi  9299  unxpwdom2  9523  cnfcomlem  9634  djuun  9861  ackbij2lem2  10175  ackbij2lem3  10176  fin4en1  10244  enfin2i  10256  hashfacenOLD  14351  gsumpropd2lem  18533  symgfixf1  19217  f1omvdmvd  19223  f1omvdconj  19226  pmtrfb  19245  symggen  19250  symggen2  19251  psgnunilem1  19273  basqtop  23060  reghmph  23142  nrmhmph  23143  indishmph  23147  ordthmeolem  23150  ufldom  23311  tgpconncompeqg  23461  imasf1oxms  23843  icchmeo  24302  dvcvx  25382  dvloglem  26001  f1ocnt  31649  cycpmconjvlem  31934  cycpmconjslem2  31948  madjusmdetlem2  32349  madjusmdetlem4  32351  tpr2rico  32433  ballotlemrv  33059  reprpmtf1o  33179  hgt750lemg  33207  subfacp1lem2b  33715  subfacp1lem5  33718  poimirlem3  36071  ismtyres  36257  eldioph2lem1  41060  lnmlmic  41392  ntrclsiex  42306  ntrneiiex  42329  ssnnf1octb  43389  f1oresf1o  45493
  Copyright terms: Public domain W3C validator