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 _xE
Assertion iunxdif3 xEB=xAEB=xAB

Proof

Step Hyp Ref Expression
1 iunxdif3.1 _xE
2 inss2 AEE
3 nfcv _xA
4 3 1 nfin _xAE
5 4 1 ssrexf AEExAEyBxEyB
6 eliun yxAEBxAEyB
7 eliun yxEBxEyB
8 5 6 7 3imtr4g AEEyxAEByxEB
9 8 ssrdv AEExAEBxEB
10 2 9 ax-mp xAEBxEB
11 iuneq2 xEB=xEB=xE
12 iun0 xE=
13 11 12 eqtrdi xEB=xEB=
14 10 13 sseqtrid xEB=xAEB
15 ss0 xAEBxAEB=
16 14 15 syl xEB=xAEB=
17 16 uneq1d xEB=xAEBxAEB=xAEB
18 iunxun xAEAEB=xAEBxAEB
19 inundif AEAE=A
20 19 nfth xAEAE=A
21 3 1 nfdif _xAE
22 4 21 nfun _xAEAE
23 id AEAE=AAEAE=A
24 eqidd AEAE=AB=B
25 20 22 3 23 24 iuneq12df AEAE=AxAEAEB=xAB
26 19 25 ax-mp xAEAEB=xAB
27 18 26 eqtr3i xAEBxAEB=xAB
28 27 a1i xEB=xAEBxAEB=xAB
29 uncom xAEB=xAEB
30 un0 xAEB=xAEB
31 29 30 eqtri xAEB=xAEB
32 31 a1i xEB=xAEB=xAEB
33 17 28 32 3eqtr3rd xEB=xAEB=xAB