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

Theorem mo2 2172
Description: Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.)
Hypothesis
Ref Expression
mo2.1  |-  F/ y
ph
Assertion
Ref Expression
mo2  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem mo2
StepHypRef Expression
1 df-mo 2148 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
2 alnex 1530 . . . . 5  |-  ( A. x  -.  ph  <->  -.  E. x ph )
3 pm2.21 100 . . . . . . 7  |-  ( -. 
ph  ->  ( ph  ->  x  =  y ) )
43alimi 1546 . . . . . 6  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  x  =  y ) )
5 19.8a 1718 . . . . . 6  |-  ( A. x ( ph  ->  x  =  y )  ->  E. y A. x (
ph  ->  x  =  y ) )
64, 5syl 15 . . . . 5  |-  ( A. x  -.  ph  ->  E. y A. x ( ph  ->  x  =  y ) )
72, 6sylbir 204 . . . 4  |-  ( -. 
E. x ph  ->  E. y A. x (
ph  ->  x  =  y ) )
8 mo2.1 . . . . 5  |-  F/ y
ph
98eumo0 2167 . . . 4  |-  ( E! x ph  ->  E. y A. x ( ph  ->  x  =  y ) )
107, 9ja 153 . . 3  |-  ( ( E. x ph  ->  E! x ph )  ->  E. y A. x (
ph  ->  x  =  y ) )
118eu3 2169 . . . 4  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
1211simplbi2com 1364 . . 3  |-  ( E. y A. x (
ph  ->  x  =  y )  ->  ( E. x ph  ->  E! x ph ) )
1310, 12impbii 180 . 2  |-  ( ( E. x ph  ->  E! x ph )  <->  E. y A. x ( ph  ->  x  =  y ) )
141, 13bitri 240 1  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176   A.wal 1527   E.wex 1528   F/wnf 1531   E!weu 2143   E*wmo 2144
This theorem is referenced by:  sbmo  2173  mo3  2174  eu5  2181  moim  2189  morimv  2191  moanim  2199  mo2icl  2944  rmo2  3076  moabex  4232  dffun3  5266  dffun6f  5269  grothprim  8456  nmo  23144
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator