Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Theorem immoi 2079
 Description: "At most one" is preserved through implication (notice wff reversal).
Hypothesis
Ref Expression
immoi.1
Assertion
Ref Expression
immoi

Proof of Theorem immoi
StepHypRef Expression
1 immo 2078 . 2
2 immoi.1 . 2
31, 2mpg 1621 1
 Colors of variables: wff set class Syntax hints:   wi 3  wmo 2038 This theorem is referenced by:  moan 2083  moor 2085  mooran1 2086  mooran2 2087  2moex 2103  2euex 2104  2exeu 2109  2eu1 2112  fvex 4778  nfunsn 4792  caoprmo 5096  th3qlem2 5535  brdom3 6377  brdom5 6378  brdom4 6379  ajfuni 10730  funadj 12282  cnlnadjeui 12479 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864 This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042
Copyright terms: Public domain