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

Metamath Proof Explorer

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 ⊢ ∩ ( 𝐴 ∪ 𝐵 ) = ( ∩ 𝐴 ∩ ∩ 𝐵 )