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	⊢ Ⅎ 𝑥 𝐴
	iindif2f.2	⊢ Ⅎ 𝑥 𝐵
Assertion	iindif2f	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		iindif2f.1	⊢ Ⅎ 𝑥 𝐴
2		iindif2f.2	⊢ Ⅎ 𝑥 𝐵
3	2	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
4	3 1	r19.28zf	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) ) )
5		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) )
6	5	bicomi	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
8		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
9		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
10	8 9	xchbinxr	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ↔ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
11	10	anbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
12	4 7 11	3bitr3g	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) ) )
13		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) )
14	13	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
15		eldif	⊢ ( 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
16	12 14 15	3bitr4g	⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) ) )
17	16	eqrdv	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶 ) )