Theorem intun

Description: The class intersection of the union of two classes. Theorem 78 of Suppes p. 42. (Contributed by NM, 22-Sep-2002)

	Ref	Expression
Assertion	intun	⊢ ∩ ( 𝐴 ∪ 𝐵 ) = ( ∩ 𝐴 ∩ ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		19.26	⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) )
2		elunant	⊢ ( ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) )
3	2	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) )
4		vex	⊢ 𝑥 ∈ V
5	4	elint	⊢ ( 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) )
6	4	elint	⊢ ( 𝑥 ∈ ∩ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) )
7	5 6	anbi12i	⊢ ( ( 𝑥 ∈ ∩ 𝐴 ∧ 𝑥 ∈ ∩ 𝐵 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) )
8	1 3 7	3bitr4i	⊢ ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ( 𝑥 ∈ ∩ 𝐴 ∧ 𝑥 ∈ ∩ 𝐵 ) )
9	4	elint	⊢ ( 𝑥 ∈ ∩ ( 𝐴 ∪ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ 𝑦 ) )
10		elin	⊢ ( 𝑥 ∈ ( ∩ 𝐴 ∩ ∩ 𝐵 ) ↔ ( 𝑥 ∈ ∩ 𝐴 ∧ 𝑥 ∈ ∩ 𝐵 ) )
11	8 9 10	3bitr4i	⊢ ( 𝑥 ∈ ∩ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ ( ∩ 𝐴 ∩ ∩ 𝐵 ) )
12	11	eqriv	⊢ ∩ ( 𝐴 ∪ 𝐵 ) = ( ∩ 𝐴 ∩ ∩ 𝐵 )