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

Theorem moimi 2223
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 2222 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 immoi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1539 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 2177
This theorem is referenced by:  moan  2227  moor  2229  mooran1  2230  mooran2  2231  2moex  2247  2euex  2248  2exeu  2253  2eu1  2256  sndisj  4052  disjxsn  4054  funcnvsn  5334  nfunsn  5596  caovmo  6099  th3qlem2  6808  iunmapdisj  7695  brdom3  8198  brdom5  8199  brdom4  8200  nqerf  8599  shftfn  11615  2ndcdisj2  17239  plyexmo  19746  ajfuni  21493  funadj  22521  cnlnadjeui  22712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181
  Copyright terms: Public domain W3C validator