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

Theorem moimi 2203
Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
Hypothesis
Ref Expression
immoi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
moimi  |-  ( E* x ps  ->  E* x ph )

Proof of Theorem moimi
StepHypRef Expression
1 moim 2202 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 immoi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1538 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 2157
This theorem is referenced by:  moan  2207  moor  2209  mooran1  2210  mooran2  2211  2moex  2227  2euex  2228  2exeu  2233  2eu1  2236  sndisj  4031  disjxsn  4033  funcnvsn  5313  nfunsn  5574  caovmo  6073  th3qlem2  6781  iunmapdisj  7666  brdom3  8169  brdom5  8170  brdom4  8171  nqerf  8570  shftfn  11584  2ndcdisj2  17199  plyexmo  19709  ajfuni  21454  funadj  22482  cnlnadjeui  22673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator