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

Theorem mo2 2310
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 2286 . 2  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
2 alnex 1552 . . . . 5  |-  ( A. x  -.  ph  <->  -.  E. x ph )
3 pm2.21 102 . . . . . . 7  |-  ( -. 
ph  ->  ( ph  ->  x  =  y ) )
43alimi 1568 . . . . . 6  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  x  =  y ) )
5 19.8a 1762 . . . . . 6  |-  ( A. x ( ph  ->  x  =  y )  ->  E. y A. x (
ph  ->  x  =  y ) )
64, 5syl 16 . . . . 5  |-  ( A. x  -.  ph  ->  E. y A. x ( ph  ->  x  =  y ) )
72, 6sylbir 205 . . . 4  |-  ( -. 
E. x ph  ->  E. y A. x (
ph  ->  x  =  y ) )
8 mo2.1 . . . . 5  |-  F/ y
ph
98eumo0 2305 . . . 4  |-  ( E! x ph  ->  E. y A. x ( ph  ->  x  =  y ) )
107, 9ja 155 . . 3  |-  ( ( E. x ph  ->  E! x ph )  ->  E. y A. x (
ph  ->  x  =  y ) )
118eu3 2307 . . . 4  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
1211simplbi2com 1383 . . 3  |-  ( E. y A. x (
ph  ->  x  =  y )  ->  ( E. x ph  ->  E! x ph ) )
1310, 12impbii 181 . 2  |-  ( ( E. x ph  ->  E! x ph )  <->  E. y A. x ( ph  ->  x  =  y ) )
141, 13bitri 241 1  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177   A.wal 1549   E.wex 1550   F/wnf 1553   E!weu 2281   E*wmo 2282
This theorem is referenced by:  sbmo  2311  mo3  2312  eu5  2319  moim  2327  morimv  2329  moanim  2337  mo2icl  3113  rmo2  3246  moabex  4422  dffun3  5465  dffun6f  5468  grothprim  8709  nmo  23973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286
  Copyright terms: Public domain W3C validator