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
Assertion
Ref Expression
mo2
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem mo2
StepHypRef Expression
1 df-mo 2161 . 2
2 alnex 1533 . . . . 5
3 pm2.21 100 . . . . . . 7
43alimi 1549 . . . . . 6
5 19.8a 1730 . . . . . 6
64, 5syl 15 . . . . 5
72, 6sylbir 204 . . . 4
8 mo2.1 . . . . 5
98eumo0 2180 . . . 4
107, 9ja 153 . . 3
118eu3 2182 . . . 4
1211simplbi2com 1364 . . 3
1310, 12impbii 180 . 2
141, 13bitri 240 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176  wal 1530  wex 1531  wnf 1534  weu 2156  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