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

Theorem mo3 2323
Description: Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that not occur in in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Aug-2019.)
Hypothesis
Ref Expression
mo3.1
Assertion
Ref Expression
mo3
Distinct variable group:   ,

Proof of Theorem mo3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfmo1 2295 . . 3
2 mo3.1 . . . . 5
32nfmo 2301 . . . 4
4 mo2v 2289 . . . . 5
5 sp 1859 . . . . . . . 8
6 spsbim 2135 . . . . . . . . 9
7 equsb3 2176 . . . . . . . . 9
86, 7syl6ib 226 . . . . . . . 8
95, 8anim12d 563 . . . . . . 7
10 equtr2 1802 . . . . . . 7
119, 10syl6 33 . . . . . 6
1211exlimiv 1722 . . . . 5
134, 12sylbi 195 . . . 4
143, 13alrimi 1877 . . 3
151, 14alrimi 1877 . 2
16 nfs1v 2181 . . . . . . . 8
17 pm3.21 448 . . . . . . . . 9
1817imim1d 75 . . . . . . . 8
1916, 18alimd 1876 . . . . . . 7
2019com12 31 . . . . . 6
2120aleximi 1653 . . . . 5
222sb8e 2168 . . . . 5
232mo2 2293 . . . . 5
2421, 22, 233imtr4g 270 . . . 4
25 moabs 2315 . . . 4
2624, 25sylibr 212 . . 3
2726alcoms 1843 . 2
2815, 27impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  F/wnf 1616  [wsb 1739  E*wmo 2283
This theorem is referenced by:  mo  2325  eu2  2326  mo4f  2336  mopickOLD  2357  2mo  2373  2moOLD  2374  rmo3  3429  isarep2  5673  mo5f  27383  rmo3f  27394  rmo4fOLD  27395  pm14.12  31328  bnj580  33971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator