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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) )