MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moim Unicode version

Theorem moim 2339
Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
Assertion
Ref Expression
moim

Proof of Theorem moim
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 imim1 76 . . . 4
21al2imi 1636 . . 3
32eximdv 1710 . 2
4 mo2v 2289 . 2
5 mo2v 2289 . 2
63, 4, 53imtr4g 270 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  E.wex 1612  E*wmo 2283
This theorem is referenced by:  moimi  2340  euimmo  2343  moexex  2363  rmoim  3299  rmoimi2  3301  disjss1  4428  disjss3  4451  reusv1  4652  reusv2lem1  4653  funmo  5609  brdom6disj  8931  uptx  20126  taylf  22756  moimd  27385  ssrmo  27393  funressnfv  32213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator