Theorem iunxdif3 28171

Description: An indexed union where some terms are the empty set. See iunxdif2 4345 (Contributed by Thierry Arnoux, 4-May-2020.)

Hypothesis

Ref	Expression
iunxdif3.1	|- F/_ x E

Assertion

Ref	Expression
iunxdif3	|- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   E( x)

Proof of Theorem iunxdif3

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss2 3684	. . . . . 6 |- ( A i^i E ) C_ E
2	1	nfth 1673	. . . . . . 7 |- F/ y ( A i^i E ) C_ E
3		nfcv 2585	. . . . . . 7 |- F/_ y U_ x e. ( A i^i E ) B
4		nfcv 2585	. . . . . . 7 |- F/_ y U_ x e. E B
5		nfcv 2585	. . . . . . . . . 10 |- F/_ x A
6		iunxdif3.1	. . . . . . . . . 10 |- F/_ x E
7	5, 6	nfin 3670	. . . . . . . . 9 |- F/_ x ( A i^i E )
8	7, 6	ssrexf 3525	. . . . . . . 8 |- ( ( A i^i E ) C_ E -> ( E. x e. ( A i^i E ) y e. B -> E. x e. E y e. B ) )
9		eliun 4302	. . . . . . . 8 |- ( y e. U_ x e. ( A i^i E ) B <-> E. x e. ( A i^i E ) y e. B )
10		eliun 4302	. . . . . . . 8 |- ( y e. U_ x e. E B <-> E. x e. E y e. B )
11	8, 9, 10	3imtr4g 274	. . . . . . 7 |- ( ( A i^i E ) C_ E -> ( y e. U_ x e. ( A i^i E ) B -> y e. U_ x e. E B ) )
12	2, 3, 4, 11	ssrd 3470	. . . . . 6 |- ( ( A i^i E ) C_ E -> U_ x e. ( A i^i E ) B C_ U_ x e. E B )
13	1, 12	ax-mp 5	. . . . 5 |- U_ x e. ( A i^i E ) B C_ U_ x e. E B
14		iuneq2 4314	. . . . . 6 |- ( A. x e. E B = (/) -> U_ x e. E B = U_ x e. E (/) )
15		iun0 4353	. . . . . 6 |- U_ x e. E (/) = (/)
16	14, 15	syl6eq 2480	. . . . 5 |- ( A. x e. E B = (/) -> U_ x e. E B = (/) )
17	13, 16	syl5sseq 3513	. . . 4 |- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B C_ (/) )
18		ss0 3794	. . . 4 |- ( U_ x e. ( A i^i E ) B C_ (/) -> U_ x e. ( A i^i E ) B = (/) )
19	17, 18	syl 17	. . 3 |- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B = (/) )
20	19	uneq1d 3620	. 2 |- ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = ( (/) u. U_ x e. ( A \ E ) B ) )
21		iunxun 4382	. . . 4 |- U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B )
22		inundif 3874	. . . . 5 |- ( ( A i^i E ) u. ( A \ E ) ) = A
23	22	nfth 1673	. . . . . 6 |- F/ x ( ( A i^i E ) u. ( A \ E ) ) = A
24	5, 6	nfdif 3587	. . . . . . 7 |- F/_ x ( A \ E )
25	7, 24	nfun 3623	. . . . . 6 |- F/_ x ( ( A i^i E ) u. ( A \ E ) )
26	22	a1i 11	. . . . . 6 |- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> ( ( A i^i E ) u. ( A \ E ) ) = A )
27		eqidd 2424	. . . . . 6 |- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> B = B )
28	23, 25, 5, 26, 27	iuneq12df 4321	. . . . 5 |- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B )
29	22, 28	ax-mp 5	. . . 4 |- U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B
30	21, 29	eqtr3i 2454	. . 3 |- ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B
31	30	a1i 11	. 2 |- ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B )
32		uncom 3611	. . . 4 |- ( (/) u. U_ x e. ( A \ E ) B ) = ( U_ x e. ( A \ E ) B u. (/) )
33		un0 3788	. . . 4 |- ( U_ x e. ( A \ E ) B u. (/) ) = U_ x e. ( A \ E ) B
34	32, 33	eqtri 2452	. . 3 |- ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B
35	34	a1i 11	. 2 |- ( A. x e. E B = (/) -> ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B )
36	20, 31, 35	3eqtr3rd 2473	1 |- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )

Syntax hints:   -> wi 4   = wceq 1438   e. wcel 1869   F/_wnfc 2571   A.wral 2776   E.wrex 2777   \ cdif 3434   u. cun 3435   i^i cin 3436   C_ wss 3437   (/)c0 3762   U_ciun 4297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-iun 4299

This theorem is referenced by:  aciunf1  28261