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

Theorem moim 2202
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 1551 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1612 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 nfv 1609 . . 3  |-  F/ y ps
54mo2 2185 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
6 nfv 1609 . . 3  |-  F/ y
ph
76mo2 2185 . 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 1530   E.wex 1531    = wceq 1632   E*wmo 2157
This theorem is referenced by:  moimi  2203  euimmo  2205  moexex  2225  rmoim  2977  rmoimi2  2979  disjss1  4015  disjss3  4038  reusv1  4550  reusv2lem1  4551  funmo  5287  brdom6disj  8173  uptx  17335  taylf  19756  moimd  23161  ssrmo  23164  funressnfv  28096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator