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

Theorem mo2 2185
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 2161 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
2 alnex 1533 . . . . 5  |-  ( A. x  -.  ph  <->  -.  E. x ph )
3 pm2.21 100 . . . . . . 7  |-  ( -. 
ph  ->  ( ph  ->  x  =  y ) )
43alimi 1549 . . . . . 6  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  x  =  y ) )
5 19.8a 1730 . . . . . 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 2180 . . . 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 2182 . . . 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 1530   E.wex 1531   F/wnf 1534   E!weu 2156   E*wmo 2157
This theorem is referenced by:  sbmo  2186  mo3  2187  eu5  2194  moim  2202  morimv  2204  moanim  2212  mo2icl  2957  rmo2  3089  moabex  4248  dffun3  5282  dffun6f  5285  grothprim  8472  nmo  23160
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