Metamath Proof Explorer

Theorem dfiin2g

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009)

Ref Expression
Assertion dfiin2g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A w ∈ B ↔ ∀ x x ∈ A → w ∈ B
2 df-ral ⊢ ∀ x ∈ A B ∈ C ↔ ∀ x x ∈ A → B ∈ C
3 clel4g ⊢ B ∈ C → w ∈ B ↔ ∀ z z = B → w ∈ z
4 3 imim2i ⊢ x ∈ A → B ∈ C → x ∈ A → w ∈ B ↔ ∀ z z = B → w ∈ z
5 4 pm5.74d ⊢ x ∈ A → B ∈ C → x ∈ A → w ∈ B ↔ x ∈ A → ∀ z z = B → w ∈ z
6 5 alimi ⊢ ∀ x x ∈ A → B ∈ C → ∀ x x ∈ A → w ∈ B ↔ x ∈ A → ∀ z z = B → w ∈ z
7 albi ⊢ ∀ x x ∈ A → w ∈ B ↔ x ∈ A → ∀ z z = B → w ∈ z → ∀ x x ∈ A → w ∈ B ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
8 6 7 syl ⊢ ∀ x x ∈ A → B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
9 2 8 sylbi ⊢ ∀ x ∈ A B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
10 df-ral ⊢ ∀ x ∈ A z = B → w ∈ z ↔ ∀ x x ∈ A → z = B → w ∈ z
11 10 albii ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ z ∀ x x ∈ A → z = B → w ∈ z
12 alcom ⊢ ∀ x ∀ z x ∈ A → z = B → w ∈ z ↔ ∀ z ∀ x x ∈ A → z = B → w ∈ z
13 11 12 bitr4i ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ x ∀ z x ∈ A → z = B → w ∈ z
14 r19.23v ⊢ ∀ x ∈ A z = B → w ∈ z ↔ ∃ x ∈ A z = B → w ∈ z
15 vex ⊢ z ∈ V
16 eqeq1 ⊢ y = z → y = B ↔ z = B
17 16 rexbidv ⊢ y = z → ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
18 15 17 elab ⊢ z ∈ y | ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
19 18 imbi1i ⊢ z ∈ y | ∃ x ∈ A y = B → w ∈ z ↔ ∃ x ∈ A z = B → w ∈ z
20 14 19 bitr4i ⊢ ∀ x ∈ A z = B → w ∈ z ↔ z ∈ y | ∃ x ∈ A y = B → w ∈ z
21 20 albii ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
22 19.21v ⊢ ∀ z x ∈ A → z = B → w ∈ z ↔ x ∈ A → ∀ z z = B → w ∈ z
23 22 albii ⊢ ∀ x ∀ z x ∈ A → z = B → w ∈ z ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
24 13 21 23 3bitr3ri ⊢ ∀ x x ∈ A → ∀ z z = B → w ∈ z ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
25 9 24 bitrdi ⊢ ∀ x ∈ A B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
26 1 25 bitrid ⊢ ∀ x ∈ A B ∈ C → ∀ x ∈ A w ∈ B ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
27 26 abbidv ⊢ ∀ x ∈ A B ∈ C → w | ∀ x ∈ A w ∈ B = w | ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
28 df-iin ⊢ ⋂ x ∈ A B = w | ∀ x ∈ A w ∈ B
29 df-int ⊢ ⋂ y | ∃ x ∈ A y = B = w | ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
30 27 28 29 3eqtr4g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B