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

Metamath Proof Explorer

Theorem iinvdif

Description: The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018)

Ref Expression
Assertion iinvdif ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 dif0 ⊢ ( V ∖ ∅ ) = V
2 0iun ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
3 2 difeq2i ⊢ ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 ) = ( V ∖ ∅ )
4 0iin ⊢ ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) = V
5 1 3 4 3eqtr4ri ⊢ ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 )
6 iineq1 ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) )
7 iuneq1 ⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
8 7 difeq2d ⊢ ( 𝐴 = ∅ → ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 ) )
9 5 6 8 3eqtr4a ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
10 iindif2 ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
11 9 10 pm2.61ine ⊢ ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 )