Theorem iunxun 4412

Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)

Assertion

Ref	Expression
iunxun

Proof of Theorem iunxun

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexun 3683	. . . 4
2		eliun 4335	. . . . 5
3		eliun 4335	. . . . 5
4	2, 3	orbi12i 521	. . . 4
5	1, 4	bitr4i 252	. . 3
6		eliun 4335	. . 3
7		elun 3644	. . 3
8	5, 6, 7	3bitr4i 277	. 2
9	8	eqriv 2453	1

Syntax hints:  \/wo 368  =wceq 1395  e.wcel 1818  E.wrex 2808  u.cun 3473  U_ciun 4330

This theorem is referenced by:  iunsuc  4965  funiunfv  6160  iunfi  7828  kmlem11  8561  ackbij1lem9  8629  fsum2dlem  13585  fsumiun  13635  fprod2dlem  13784  prmreclem4  14437  fiuncmp  19904  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  voliunlem1  21960  uniioombllem4  21995  iuninc  27428  ofpreima2  27508  indval2  28028  sigaclfu2  28121  measvuni  28185  cvmliftlem10  28739  mrsubvrs  28882  mblfinlem2  30052  iunxprg  32302

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-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-un 3480  df-iun 4332