Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjin Unicode version

Theorem disjin 25057
Description: If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.)
Assertion
Ref Expression
disjin

Proof of Theorem disjin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 inss1 3606 . . . . . . 7
21sseli 3389 . . . . . 6
32anim2i 554 . . . . 5
43ax-gen 1570 . . . 4
54rmoimi2 3198 . . 3
65alimi 1583 . 2
7 df-disj 4289 . 2
8 df-disj 4289 . 2
96, 7, 83imtr4i 259 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  A.wal 1564  e.wcel 1732  E*wrmo 2762  i^icin 3364  Disj_wdisj 4288
This theorem is referenced by:  measinblem  25814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-rmo 2767  df-v 3017  df-in 3372  df-ss 3379  df-disj 4289
  Copyright terms: Public domain W3C validator