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

Theorem moim 2328
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 1607 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1677 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 mo2v 2269 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
5 mo2v 2269 . 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 1368   E.wex 1587   E*wmo 2263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-eu 2266  df-mo 2267
This theorem is referenced by:  moimi  2329  euimmo  2332  moexex  2358  moexexOLD  2359  rmoim  3266  rmoimi2  3268  disjss1  4379  disjss3  4402  reusv1  4603  reusv2lem1  4604  funmo  5545  brdom6disj  8813  uptx  19333  taylf  21962  moimd  26042  ssrmo  26050  funressnfv  30202
  Copyright terms: Public domain W3C validator