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

Metamath Proof Explorer

Theorem iindif2f

Description: Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws". (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses iindif2f.1 ⊢ Ⅎ _ x A
iindif2f.2 ⊢ Ⅎ _ x B
Assertion iindif2f ⊢ A ≠ ∅ → ⋂ x ∈ A B ∖ C = B ∖ ⋃ x ∈ A C

Proof

Step Hyp Ref Expression
1 iindif2f.1 ⊢ Ⅎ _ x A
2 iindif2f.2 ⊢ Ⅎ _ x B
3 2 nfcri ⊢ Ⅎ x y ∈ B
4 3 1 r19.28zf ⊢ A ≠ ∅ → ∀ x ∈ A y ∈ B ∧ ¬ y ∈ C ↔ y ∈ B ∧ ∀ x ∈ A ¬ y ∈ C
5 eldif ⊢ y ∈ B ∖ C ↔ y ∈ B ∧ ¬ y ∈ C
6 5 bicomi ⊢ y ∈ B ∧ ¬ y ∈ C ↔ y ∈ B ∖ C
7 6 ralbii ⊢ ∀ x ∈ A y ∈ B ∧ ¬ y ∈ C ↔ ∀ x ∈ A y ∈ B ∖ C
8 ralnex ⊢ ∀ x ∈ A ¬ y ∈ C ↔ ¬ ∃ x ∈ A y ∈ C
9 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
10 8 9 xchbinxr ⊢ ∀ x ∈ A ¬ y ∈ C ↔ ¬ y ∈ ⋃ x ∈ A C
11 10 anbi2i ⊢ y ∈ B ∧ ∀ x ∈ A ¬ y ∈ C ↔ y ∈ B ∧ ¬ y ∈ ⋃ x ∈ A C
12 4 7 11 3bitr3g ⊢ A ≠ ∅ → ∀ x ∈ A y ∈ B ∖ C ↔ y ∈ B ∧ ¬ y ∈ ⋃ x ∈ A C
13 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ∖ C ↔ ∀ x ∈ A y ∈ B ∖ C
14 13 elv ⊢ y ∈ ⋂ x ∈ A B ∖ C ↔ ∀ x ∈ A y ∈ B ∖ C
15 eldif ⊢ y ∈ B ∖ ⋃ x ∈ A C ↔ y ∈ B ∧ ¬ y ∈ ⋃ x ∈ A C
16 12 14 15 3bitr4g ⊢ A ≠ ∅ → y ∈ ⋂ x ∈ A B ∖ C ↔ y ∈ B ∖ ⋃ x ∈ A C
17 16 eqrdv ⊢ A ≠ ∅ → ⋂ x ∈ A B ∖ C = B ∖ ⋃ x ∈ A C