Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disji2f Structured version   Unicode version

Theorem disji2f 27097
 Description: Property of a disjoint collection: if and , and , then and are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.)
Hypotheses
Ref Expression
disjif.1
disjif.2
Assertion
Ref Expression
disji2f Disj
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem disji2f
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ne 2657 . . 3
2 disjors 4426 . . . . . 6 Disj
3 equequ1 1742 . . . . . . . 8
4 csbeq1 3431 . . . . . . . . . . 11
5 csbid 3436 . . . . . . . . . . 11
64, 5syl6eq 2517 . . . . . . . . . 10
76ineq1d 3692 . . . . . . . . 9
87eqeq1d 2462 . . . . . . . 8
93, 8orbi12d 709 . . . . . . 7
10 eqeq2 2475 . . . . . . . 8
11 nfcv 2622 . . . . . . . . . . 11
12 disjif.1 . . . . . . . . . . 11
13 disjif.2 . . . . . . . . . . 11
1411, 12, 13csbhypf 3447 . . . . . . . . . 10
1514ineq2d 3693 . . . . . . . . 9
1615eqeq1d 2462 . . . . . . . 8
1710, 16orbi12d 709 . . . . . . 7
189, 17rspc2v 3216 . . . . . 6
192, 18syl5bi 217 . . . . 5 Disj
2019impcom 430 . . . 4 Disj
2120ord 377 . . 3 Disj
221, 21syl5bi 217 . 2 Disj
23223impia 1188 1 Disj
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 368   wa 369   w3a 968   wceq 1374   wcel 1762  wnfc 2608   wne 2655  wral 2807  csb 3428   cin 3468  c0 3778  Disj wdisj 4410 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-in 3476  df-nul 3779  df-disj 4411 This theorem is referenced by:  disjif  27098
 Copyright terms: Public domain W3C validator