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

Theorem moim 2359
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 1698 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1775 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 mo2v 2317 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
5 mo2v 2317 . 2  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
63, 4, 53imtr4g 278 1  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1453   E.wex 1674   E*wmo 2311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679  df-eu 2314  df-mo 2315
This theorem is referenced by:  moimi  2360  euimmo  2362  moexex  2381  rmoim  3251  rmoimi2  3253  disjss1  4393  disjss3  4415  reusv1  4617  reusv2lem1  4618  funmo  5617  brdom6disj  8986  uptx  20689  taylf  23365  moimd  28171  ssrmo  28179  funressnfv  38667
  Copyright terms: Public domain W3C validator