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

Theorem moimi 2190
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 2189 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 immoi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1535 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 2144
This theorem is referenced by:  moan  2194  moor  2196  mooran1  2197  mooran2  2198  2moex  2214  2euex  2215  2exeu  2220  2eu1  2223  sndisj  4015  disjxsn  4017  funcnvsn  5297  nfunsn  5558  caovmo  6057  th3qlem2  6765  iunmapdisj  7650  brdom3  8153  brdom5  8154  brdom4  8155  nqerf  8554  shftfn  11568  2ndcdisj2  17183  plyexmo  19693  ajfuni  21438  funadj  22466  cnlnadjeui  22657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator