Theorem iindif2

Description: Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in Enderton p. 31. Use uniiun to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006)

	Ref	Expression
Assertion	iindif2	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) ) )
2		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
3	2	bicomi	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
4	3	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
5		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
6		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
7	5 6	xchbinxr	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
8	7	anbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
9	1 4 8	3bitr3g	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) ) )
10		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) )
11	10	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
12		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
13	9 11 12	3bitr4g	⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) ) )
14	13	eqrdv	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) )