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

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

Proof of Theorem moimi
StepHypRef Expression
1 moim 2358 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 moimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1681 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E*wmo 2310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678  df-eu 2313  df-mo 2314
This theorem is referenced by:  morimOLD  2360  moan  2363  moor  2365  mooran1  2366  mooran2  2367  moaneu  2372  2moex  2382  2euex  2383  2exeu  2388  sndisj  4407  disjxsn  4409  fununmo  5643  funcnvsn  5645  nfunsn  5918  caovmo  6532  iunmapdisj  8479  brdom3  8981  brdom5  8982  brdom4  8983  nqerf  9380  shftfn  13184  2ndcdisj2  20520  plyexmo  23314  ajfuni  26549  funadj  27587  cnlnadjeui  27778
  Copyright terms: Public domain W3C validator