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

Theorem disjor 4436
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
Distinct variable groups:   , ,   ,   ,

Proof of Theorem disjor
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-disj 4423 . 2
2 ralcom4 3128 . . 3
3 orcom 387 . . . . . . 7
4 df-or 370 . . . . . . 7
5 neq0 3795 . . . . . . . . . 10
6 elin 3686 . . . . . . . . . . 11
76exbii 1667 . . . . . . . . . 10
85, 7bitri 249 . . . . . . . . 9
98imbi1i 325 . . . . . . . 8
10 19.23v 1760 . . . . . . . 8
119, 10bitr4i 252 . . . . . . 7
123, 4, 113bitri 271 . . . . . 6
1312ralbii 2888 . . . . 5
14 ralcom4 3128 . . . . 5
1513, 14bitri 249 . . . 4
1615ralbii 2888 . . 3
17 disjmo.1 . . . . . 6
1817eleq2d 2527 . . . . 5
1918rmo4 3292 . . . 4
2019albii 1640 . . 3
212, 16, 203bitr4i 277 . 2
221, 21bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  A.wral 2807  E*wrmo 2810  i^icin 3474   c0 3784  Disj_wdisj 4422
This theorem is referenced by:  disjmoOLD  4437  disjors  4438  disjxiun  4449  disjxun  4450  otsndisj  4757  otiunsndisj  4758  qsdisj2  7408  cshwsdisj  14583  dyadmbl  22009  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  numclwwlkdisj  25080  disjnf  27433  disjorsf  27441  mblfinlem2  30052  otiunsndisjX  32301
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  ax-ext 2435
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  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rmo 2815  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785  df-disj 4423
  Copyright terms: Public domain W3C validator