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

Theorem moim 2337
Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
Assertion
Ref Expression
moim  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )

Proof of Theorem moim
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 imim1 76 . . . 4  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  x  =  y )  -> 
( ph  ->  x  =  y ) ) )
21al2imi 1641 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1715 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 mo2v 2291 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
5 mo2v 2291 . 2  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
63, 4, 53imtr4g 270 1  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396   E.wex 1617   E*wmo 2285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-eu 2288  df-mo 2289
This theorem is referenced by:  moimi  2338  euimmo  2340  moexex  2360  rmoim  3296  rmoimi2  3298  disjss1  4416  disjss3  4438  reusv1  4637  reusv2lem1  4638  funmo  5586  brdom6disj  8901  uptx  20292  taylf  22922  moimd  27583  ssrmo  27591  funressnfv  32452
  Copyright terms: Public domain W3C validator