This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = y -> C = D )
Assertion iunxdif2 
|- ( A. x e. A E. y e. ( A \ B ) C C_ D -> U_ y e. ( A \ B ) D = U_ x e. A C )

Proof

Step Hyp Ref Expression
1 iunxdif2.1 
 |-  ( x = y -> C = D )
2 iunss2 
 |-  ( A. x e. A E. y e. ( A \ B ) C C_ D -> U_ x e. A C C_ U_ y e. ( A \ B ) D )
3 difss 
 |-  ( A \ B ) C_ A
4 iunss1 
 |-  ( ( A \ B ) C_ A -> U_ y e. ( A \ B ) D C_ U_ y e. A D )
5 3 4 ax-mp 
 |-  U_ y e. ( A \ B ) D C_ U_ y e. A D
6 1 cbviunv 
 |-  U_ x e. A C = U_ y e. A D
7 5 6 sseqtrri 
 |-  U_ y e. ( A \ B ) D C_ U_ x e. A C
8 2 7 jctil 
 |-  ( A. x e. A E. y e. ( A \ B ) C C_ D -> ( U_ y e. ( A \ B ) D C_ U_ x e. A C /\ U_ x e. A C C_ U_ y e. ( A \ B ) D ) )
9 eqss 
 |-  ( U_ y e. ( A \ B ) D = U_ x e. A C <-> ( U_ y e. ( A \ B ) D C_ U_ x e. A C /\ U_ x e. A C C_ U_ y e. ( A \ B ) D ) )
10 8 9 sylibr 
 |-  ( A. x e. A E. y e. ( A \ B ) C C_ D -> U_ y e. ( A \ B ) D = U_ x e. A C )