Metamath Proof Explorer

Theorem intpr

Description: The intersection of a pair is the intersection of its members. Theorem 71 of Suppes p. 42. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypotheses intpr.1 ⊢ A ∈ V
intpr.2 ⊢ B ∈ V
Assertion intpr ⊢ ⋂ A B = A ∩ B

Proof

Step Hyp Ref Expression
1 intpr.1 ⊢ A ∈ V
2 intpr.2 ⊢ B ∈ V
3 19.26 ⊢ ∀ y y = A → x ∈ y ∧ y = B → x ∈ y ↔ ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y
4 vex ⊢ y ∈ V
5 4 elpr ⊢ y ∈ A B ↔ y = A ∨ y = B
6 5 imbi1i ⊢ y ∈ A B → x ∈ y ↔ y = A ∨ y = B → x ∈ y
7 jaob ⊢ y = A ∨ y = B → x ∈ y ↔ y = A → x ∈ y ∧ y = B → x ∈ y
8 6 7 bitri ⊢ y ∈ A B → x ∈ y ↔ y = A → x ∈ y ∧ y = B → x ∈ y
9 8 albii ⊢ ∀ y y ∈ A B → x ∈ y ↔ ∀ y y = A → x ∈ y ∧ y = B → x ∈ y
10 1 clel4 ⊢ x ∈ A ↔ ∀ y y = A → x ∈ y
11 2 clel4 ⊢ x ∈ B ↔ ∀ y y = B → x ∈ y
12 10 11 anbi12i ⊢ x ∈ A ∧ x ∈ B ↔ ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y
13 3 9 12 3bitr4i ⊢ ∀ y y ∈ A B → x ∈ y ↔ x ∈ A ∧ x ∈ B
14 vex ⊢ x ∈ V
15 14 elint ⊢ x ∈ ⋂ A B ↔ ∀ y y ∈ A B → x ∈ y
16 elin ⊢ x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B
17 13 15 16 3bitr4i ⊢ x ∈ ⋂ A B ↔ x ∈ A ∩ B
18 17 eqriv ⊢ ⋂ A B = A ∩ B