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 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion iunxdif2 ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ⊆ 𝐷 → ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 iunxdif2.1 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
2 iunss2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 )
3 difss ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
4 iunss1 ⊢ ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 → ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ⊆ ∪ 𝑦 ∈ 𝐴 𝐷 )
5 3 4 ax-mp ⊢ ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ⊆ ∪ 𝑦 ∈ 𝐴 𝐷
6 1 cbviunv ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐴 𝐷
7 5 6 sseqtrri ⊢ ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶
8 2 7 jctil ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ⊆ 𝐷 → ( ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ) )
9 eqss ⊢ ( ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ( ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 ) )
10 8 9 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ⊆ 𝐷 → ∪ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶 )