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

Theorem moim 2189
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 70 . . . 4  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  x  =  y )  -> 
( ph  ->  x  =  y ) ) )
21al2imi 1548 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1608 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 nfv 1605 . . 3  |-  F/ y ps
54mo2 2172 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
6 nfv 1605 . . 3  |-  F/ y
ph
76mo2 2172 . 2  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
83, 5, 73imtr4g 261 1  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   E.wex 1528    = wceq 1623   E*wmo 2144
This theorem is referenced by:  moimi  2190  euimmo  2192  moexex  2212  rmoim  2964  rmoimi2  2966  disjss1  3999  disjss3  4022  reusv1  4534  reusv2lem1  4535  funmo  5271  brdom6disj  8157  uptx  17319  taylf  19740  moimd  23145  ssrmo  23148  funressnfv  27991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator