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

Metamath Proof Explorer

Theorem intprg

Description: The intersection of a pair is the intersection of its members. Closed form of intpr . Theorem 71 of Suppes p. 42. (Contributed by FL, 27-Apr-2008) (Proof shortened by BJ, 1-Sep-2024)

Ref Expression
Assertion intprg ⊢ A ∈ V ∧ B ∈ W → ⋂ A B = A ∩ B

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 elint ⊢ x ∈ ⋂ A B ↔ ∀ y y ∈ A B → x ∈ y
3 vex ⊢ y ∈ V
4 3 elpr ⊢ y ∈ A B ↔ y = A ∨ y = B
5 4 imbi1i ⊢ y ∈ A B → x ∈ y ↔ y = A ∨ y = B → x ∈ y
6 jaob ⊢ y = A ∨ y = B → x ∈ y ↔ y = A → x ∈ y ∧ y = B → x ∈ y
7 5 6 bitri ⊢ y ∈ A B → x ∈ y ↔ y = A → x ∈ y ∧ y = B → x ∈ y
8 7 albii ⊢ ∀ y y ∈ A B → x ∈ y ↔ ∀ y y = A → x ∈ y ∧ y = B → x ∈ y
9 19.26 ⊢ ∀ y y = A → x ∈ y ∧ y = B → x ∈ y ↔ ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y
10 2 8 9 3bitri ⊢ x ∈ ⋂ A B ↔ ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y
11 elin ⊢ x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B
12 clel4g ⊢ A ∈ V → x ∈ A ↔ ∀ y y = A → x ∈ y
13 clel4g ⊢ B ∈ W → x ∈ B ↔ ∀ y y = B → x ∈ y
14 12 13 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → x ∈ A ∧ x ∈ B ↔ ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y
15 11 14 bitr2id ⊢ A ∈ V ∧ B ∈ W → ∀ y y = A → x ∈ y ∧ ∀ y y = B → x ∈ y ↔ x ∈ A ∩ B
16 10 15 bitrid ⊢ A ∈ V ∧ B ∈ W → x ∈ ⋂ A B ↔ x ∈ A ∩ B
17 16 alrimiv ⊢ A ∈ V ∧ B ∈ W → ∀ x x ∈ ⋂ A B ↔ x ∈ A ∩ B
18 dfcleq ⊢ ⋂ A B = A ∩ B ↔ ∀ x x ∈ ⋂ A B ↔ x ∈ A ∩ B
19 17 18 sylibr ⊢ A ∈ V ∧ B ∈ W → ⋂ A B = A ∩ B