Theorem iundif2

Description: Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in Enderton p. 31. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

	Ref	Expression
Assertion	iundif2	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
2	1	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
3		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) )
4		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
5		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
6	5	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
7	4 6	xchbinxr	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 )
8	7	anbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
9	2 3 8	3bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
10		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
11		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
12	9 10 11	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
13	12	eqriv	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶 )