Theorem iunxdif3 28223

Description: An indexed union where some terms are the empty set. See iunxdif2 4339. (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 3664	. . . . . 6 |- ( A i^i E ) C_ E
2	1	nfth 1686	. . . . . . 7 |- F/ y ( A i^i E ) C_ E
3		nfcv 2602	. . . . . . 7 |- F/_ y U_ x e. ( A i^i E ) B
4		nfcv 2602	. . . . . . 7 |- F/_ y U_ x e. E B
5		nfcv 2602	. . . . . . . . . 10 |- F/_ x A
6		iunxdif3.1	. . . . . . . . . 10 |- F/_ x E
7	5, 6	nfin 3650	. . . . . . . . 9 |- F/_ x ( A i^i E )
8	7, 6	ssrexf 3503	. . . . . . . 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 4296	. . . . . . . 8 |- ( y e. U_ x e. ( A i^i E ) B <-> E. x e. ( A i^i E ) y e. B )
10		eliun 4296	. . . . . . . 8 |- ( y e. U_ x e. E B <-> E. x e. E y e. B )
11	8, 9, 10	3imtr4g 278	. . . . . . 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 3448	. . . . . 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 4308	. . . . . 6 |- ( A. x e. E B = (/) -> U_ x e. E B = U_ x e. E (/) )
15		iun0 4347	. . . . . 6 |- U_ x e. E (/) = (/)
16	14, 15	syl6eq 2511	. . . . 5 |- ( A. x e. E B = (/) -> U_ x e. E B = (/) )
17	13, 16	syl5sseq 3491	. . . 4 |- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B C_ (/) )
18		ss0 3776	. . . 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 3598	. 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 4376	. . . 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 3856	. . . . 5 |- ( ( A i^i E ) u. ( A \ E ) ) = A
23	22	nfth 1686	. . . . . 6 |- F/ x ( ( A i^i E ) u. ( A \ E ) ) = A
24	5, 6	nfdif 3565	. . . . . . 7 |- F/_ x ( A \ E )
25	7, 24	nfun 3601	. . . . . 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 2462	. . . . . 6 |- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> B = B )
28	23, 25, 5, 26, 27	iuneq12df 4315	. . . . 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 2485	. . 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 3589	. . . 4 |- ( (/) u. U_ x e. ( A \ E ) B ) = ( U_ x e. ( A \ E ) B u. (/) )
33		un0 3770	. . . 4 |- ( U_ x e. ( A \ E ) B u. (/) ) = U_ x e. ( A \ E ) B
34	32, 33	eqtri 2483	. . 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 2504	1 |- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )

Syntax hints:   -> wi 4   = wceq 1454   e. wcel 1897   F/_wnfc 2589   A.wral 2748   E.wrex 2749   \ cdif 3412   u. cun 3413   i^i cin 3414   C_ wss 3415   (/)c0 3742   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-iun 4293

This theorem is referenced by:  aciunf1  28313