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

Metamath Proof Explorer

Theorem iindif1

Description: Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Assertion iindif1 ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( ∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 r19.27zv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ) )
2 eldif ⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
4 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
5 4 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
6 5 anbi1i ⊢ ( ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
7 1 3 6 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ) )
8 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) )
9 8 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
10 eldif ⊢ ( 𝑦 ∈ ( ∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
11 7 9 10 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ 𝑦 ∈ ( ∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶 ) ) )
12 11 eqrdv ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( ∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶 ) )