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

Theorem disjor 4198
 Description: Two ways to say that a collection for is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
Hypothesis
Ref Expression
disjmo.1
Assertion
Ref Expression
disjor Disj
Distinct variable groups:   ,,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem disjor
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-disj 4185 . 2 Disj
2 ralcom4 2976 . . 3
3 orcom 378 . . . . . . 7
4 df-or 361 . . . . . . 7
5 neq0 3640 . . . . . . . . . 10
6 elin 3532 . . . . . . . . . . 11
76exbii 1593 . . . . . . . . . 10
85, 7bitri 242 . . . . . . . . 9
98imbi1i 317 . . . . . . . 8
10 19.23v 1915 . . . . . . . 8
119, 10bitr4i 245 . . . . . . 7
123, 4, 113bitri 264 . . . . . 6
1312ralbii 2731 . . . . 5
14 ralcom4 2976 . . . . 5
1513, 14bitri 242 . . . 4
1615ralbii 2731 . . 3
17 disjmo.1 . . . . . 6
1817eleq2d 2505 . . . . 5
1918rmo4 3129 . . . 4
2019albii 1576 . . 3
212, 16, 203bitr4i 270 . 2
221, 21bitr4i 245 1 Disj
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359   wa 360  wal 1550  wex 1551   wceq 1653   wcel 1726  wral 2707  wrmo 2710   cin 3321  c0 3630  Disj wdisj 4184 This theorem is referenced by:  disjmoOLD  4199  disjors  4200  disjxiun  4211  disjxun  4212  qsdisj2  6984  dyadmbl  19494  disjorsf  24024  mblfinlem2  26246  otsndisj  28068  otiunsndisj  28069  otiunsndisjX  28070  cshwsdisj  28307  2spotdisj  28512  2spotiundisj  28513  2spotmdisj  28519 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rmo 2715  df-v 2960  df-dif 3325  df-in 3329  df-nul 3631  df-disj 4185
 Copyright terms: Public domain W3C validator