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

Theorem moim 2318
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 79 . . . 4  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  x  =  y )  -> 
( ph  ->  x  =  y ) ) )
21al2imi 1683 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1757 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 mo2v 2273 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
5 mo2v 2273 . 2  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
63, 4, 53imtr4g 273 1  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   E.wex 1659   E*wmo 2267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271
This theorem is referenced by:  moimi  2319  euimmo  2321  moexex  2341  rmoim  3277  rmoimi2  3279  disjss1  4403  disjss3  4425  reusv1  4625  reusv2lem1  4626  funmo  5617  brdom6disj  8958  uptx  20571  taylf  23181  moimd  27957  ssrmo  27965  funressnfv  38029
  Copyright terms: Public domain W3C validator