Theorem iunxdif3 27637

Description: An indexed union where some terms are the empty set. See iunxdif2 4363 (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 3705	. . . . . 6 |- ( A i^i E ) C_ E
2	1	nfth 1630	. . . . . . 7 |- F/ y ( A i^i E ) C_ E
3		nfcv 2616	. . . . . . 7 |- F/_ y U_ x e. ( A i^i E ) B
4		nfcv 2616	. . . . . . 7 |- F/_ y U_ x e. E B
5		nfcv 2616	. . . . . . . . . 10 |- F/_ x A
6		iunxdif3.1	. . . . . . . . . 10 |- F/_ x E
7	5, 6	nfin 3691	. . . . . . . . 9 |- F/_ x ( A i^i E )
8	7, 6	ssrexf 3549	. . . . . . . 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 4320	. . . . . . . 8 |- ( y e. U_ x e. ( A i^i E ) B <-> E. x e. ( A i^i E ) y e. B )
10		eliun 4320	. . . . . . . 8 |- ( y e. U_ x e. E B <-> E. x e. E y e. B )
11	8, 9, 10	3imtr4g 270	. . . . . . 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 3494	. . . . . 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 4332	. . . . . 6 |- ( A. x e. E B = (/) -> U_ x e. E B = U_ x e. E (/) )
15		iun0 4371	. . . . . 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 3537	. . . 4 |- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B C_ (/) )
18		ss0 3815	. . . 4 |- ( U_ x e. ( A i^i E ) B C_ (/) -> U_ x e. ( A i^i E ) B = (/) )
19	17, 18	syl 16	. . 3 |- ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B = (/) )
20	19	uneq1d 3643	. 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 4400	. . . 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 3894	. . . . 5 |- ( ( A i^i E ) u. ( A \ E ) ) = A
23	22	nfth 1630	. . . . . 6 |- F/ x ( ( A i^i E ) u. ( A \ E ) ) = A
24	5, 6	nfdif 3611	. . . . . . 7 |- F/_ x ( A \ E )
25	7, 24	nfun 3646	. . . . . 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 2455	. . . . . 6 |- ( ( ( A i^i E ) u. ( A \ E ) ) = A -> B = B )
28	23, 25, 5, 26, 27	iuneq12df 4339	. . . . 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 3634	. . . 4 |- ( (/) u. U_ x e. ( A \ E ) B ) = ( U_ x e. ( A \ E ) B u. (/) )
33		un0 3809	. . . 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 1398   e. wcel 1823   F/_wnfc 2602   A.wral 2804   E.wrex 2805   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3783   U_ciun 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-iun 4317

This theorem is referenced by:  aciunf1  27730