Metamath Proof Explorer


Theorem iunxdif2

Description: Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004)

Ref Expression
Hypothesis iunxdif2.1 x=yC=D
Assertion iunxdif2 xAyABCDyABD=xAC

Proof

Step Hyp Ref Expression
1 iunxdif2.1 x=yC=D
2 iunss2 xAyABCDxACyABD
3 difss ABA
4 iunss1 ABAyABDyAD
5 3 4 ax-mp yABDyAD
6 1 cbviunv xAC=yAD
7 5 6 sseqtrri yABDxAC
8 2 7 jctil xAyABCDyABDxACxACyABD
9 eqss yABD=xACyABDxACxACyABD
10 8 9 sylibr xAyABCDyABD=xAC