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 ⊢ ⋂ x ∈ A V ∖ B = V ∖ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 dif0 ⊢ V ∖ ∅ = V
2 0iun ⊢ ⋃ x ∈ ∅ B = ∅
3 2 difeq2i ⊢ V ∖ ⋃ x ∈ ∅ B = V ∖ ∅
4 0iin ⊢ ⋂ x ∈ ∅ V ∖ B = V
5 1 3 4 3eqtr4ri ⊢ ⋂ x ∈ ∅ V ∖ B = V ∖ ⋃ x ∈ ∅ B
6 iineq1 ⊢ A = ∅ → ⋂ x ∈ A V ∖ B = ⋂ x ∈ ∅ V ∖ B
7 iuneq1 ⊢ A = ∅ → ⋃ x ∈ A B = ⋃ x ∈ ∅ B
8 7 difeq2d ⊢ A = ∅ → V ∖ ⋃ x ∈ A B = V ∖ ⋃ x ∈ ∅ B
9 5 6 8 3eqtr4a ⊢ A = ∅ → ⋂ x ∈ A V ∖ B = V ∖ ⋃ x ∈ A B
10 iindif2 ⊢ A ≠ ∅ → ⋂ x ∈ A V ∖ B = V ∖ ⋃ x ∈ A B
11 9 10 pm2.61ine ⊢ ⋂ x ∈ A V ∖ B = V ∖ ⋃ x ∈ A B