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

Theorem f1odm 6595
 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 6592 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 6426 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  dom cdm 5520   Fn wfn 6320  –1-1-onto→wf1o 6324 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 210  df-an 400  df-fn 6328  df-f 6329  df-f1 6330  df-f1o 6332 This theorem is referenced by:  f1imacnv  6607  f1opw2  7382  xpcomco  8593  domss2  8663  mapen  8668  ssenen  8678  phplem4  8686  php3  8690  f1opwfi  8815  unxpwdom2  9039  cnfcomlem  9149  djuun  9342  ackbij2lem2  9654  ackbij2lem3  9655  fin4en1  9723  enfin2i  9735  hashfacen  13811  gsumpropd2lem  17884  symgfixf1  18561  f1omvdmvd  18567  f1omvdconj  18570  pmtrfb  18589  symggen  18594  symggen2  18595  psgnunilem1  18617  basqtop  22326  reghmph  22408  nrmhmph  22409  indishmph  22413  ordthmeolem  22416  ufldom  22577  tgpconncompeqg  22727  imasf1oxms  23106  icchmeo  23556  dvcvx  24633  dvloglem  25249  f1ocnt  30561  cycpmconjvlem  30843  cycpmconjslem2  30857  madjusmdetlem2  31196  madjusmdetlem4  31198  tpr2rico  31280  ballotlemrv  31902  reprpmtf1o  32022  hgt750lemg  32050  subfacp1lem2b  32556  subfacp1lem5  32559  poimirlem3  35079  ismtyres  35265  eldioph2lem1  39744  lnmlmic  40075  ntrclsiex  40799  ntrneiiex  40822  ssnnf1octb  41865  f1oresf1o  43889
 Copyright terms: Public domain W3C validator