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

Theorem moim 2325
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 1623 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ( ps  ->  x  =  y )  ->  A. x ( ph  ->  x  =  y ) ) )
32eximdv 1697 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. y A. x ( ps 
->  x  =  y
)  ->  E. y A. x ( ph  ->  x  =  y ) ) )
4 mo2v 2275 . 2  |-  ( E* x ps  <->  E. y A. x ( ps  ->  x  =  y ) )
5 mo2v 2275 . 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 1381   E.wex 1599   E*wmo 2269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604  df-eu 2272  df-mo 2273
This theorem is referenced by:  moimi  2326  euimmo  2329  moexex  2349  rmoim  3285  rmoimi2  3287  disjss1  4413  disjss3  4436  reusv1  4637  reusv2lem1  4638  funmo  5594  brdom6disj  8913  uptx  19999  taylf  22628  moimd  27257  ssrmo  27265  funressnfv  32051
  Copyright terms: Public domain W3C validator