Theorem iunin2 4394

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4383 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)

Assertion

Ref	Expression
iunin2

Distinct variable group:   ,

Proof of Theorem iunin2

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		r19.42v 3012	. . . 4
2		elin 3686	. . . . 5
3	2	rexbii 2959	. . . 4
4		eliun 4335	. . . . 5
5	4	anbi2i 694	. . . 4
6	1, 3, 5	3bitr4i 277	. . 3
7		eliun 4335	. . 3
8		elin 3686	. . 3
9	6, 7, 8	3bitr4i 277	. 2
10	9	eqriv 2453	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808  i^icin 3474  U_ciun 4330

This theorem is referenced by:  iunin1  4395  2iunin  4398  resiun1  5297  resiun2  5298  infssuni  7831  kmlem11  8561  cmpsublem  19899  cmpsub  19900  kgentopon  20039  metnrmlem3  21365  ovoliunlem1  21913  voliunlem1  21960  voliunlem2  21961  uniioombllem2  21992  uniioombllem4  21995  volsup2  22014  itg1addlem5  22107  itg1climres  22121  cvmscld  28718  cnambfre  30063  ftc1anclem6  30095  heiborlem3  30309

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-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-iun 4332