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

Theorem moimi 2327
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 2326 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 immoi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1557 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 2281
This theorem is referenced by:  moan  2331  moor  2333  mooran1  2334  mooran2  2335  2moex  2351  2euex  2352  2exeu  2357  2eu1  2360  sndisj  4196  disjxsn  4198  funcnvsn  5488  nfunsn  5753  caovmo  6276  th3qlem2  7003  iunmapdisj  7896  brdom3  8398  brdom5  8399  brdom4  8400  nqerf  8799  shftfn  11880  2ndcdisj2  17512  plyexmo  20222  ajfuni  22353  funadj  23381  cnlnadjeui  23572
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
  Copyright terms: Public domain W3C validator