Metamath Proof Explorer


Theorem iunxdif3

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

Ref Expression
Hypothesis iunxdif3.1 _ x E
Assertion iunxdif3 x E B = x A E B = x A B

Proof

Step Hyp Ref Expression
1 iunxdif3.1 _ x E
2 inss2 A E E
3 nfcv _ x A
4 3 1 nfin _ x A E
5 4 1 ssrexf A E E x A E y B x E y B
6 eliun y x A E B x A E y B
7 eliun y x E B x E y B
8 5 6 7 3imtr4g A E E y x A E B y x E B
9 8 ssrdv A E E x A E B x E B
10 2 9 ax-mp x A E B x E B
11 iuneq2 x E B = x E B = x E
12 iun0 x E =
13 11 12 eqtrdi x E B = x E B =
14 10 13 sseqtrid x E B = x A E B
15 ss0 x A E B x A E B =
16 14 15 syl x E B = x A E B =
17 16 uneq1d x E B = x A E B x A E B = x A E B
18 iunxun x A E A E B = x A E B x A E B
19 inundif A E A E = A
20 19 nfth x A E A E = A
21 3 1 nfdif _ x A E
22 4 21 nfun _ x A E A E
23 id A E A E = A A E A E = A
24 eqidd A E A E = A B = B
25 20 22 3 23 24 iuneq12df A E A E = A x A E A E B = x A B
26 19 25 ax-mp x A E A E B = x A B
27 18 26 eqtr3i x A E B x A E B = x A B
28 27 a1i x E B = x A E B x A E B = x A B
29 uncom x A E B = x A E B
30 un0 x A E B = x A E B
31 29 30 eqtri x A E B = x A E B
32 31 a1i x E B = x A E B = x A E B
33 17 28 32 3eqtr3rd x E B = x A E B = x A B