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