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