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

Metamath Proof Explorer

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