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

Theorem moimi 2330
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 2329 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 immoi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1558 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 2284
This theorem is referenced by:  moan  2334  moor  2336  mooran1  2337  mooran2  2338  2moex  2354  2euex  2355  2exeu  2360  2eu1  2363  sndisj  4206  disjxsn  4208  funcnvsn  5498  nfunsn  5763  caovmo  6286  th3qlem2  7013  iunmapdisj  7906  brdom3  8408  brdom5  8409  brdom4  8410  nqerf  8809  shftfn  11890  2ndcdisj2  17522  plyexmo  20232  ajfuni  22363  funadj  23391  cnlnadjeui  23582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288
  Copyright terms: Public domain W3C validator