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 eleq2 ⊢ z = B → w ∈ z ↔ w ∈ B
4 3 biimprcd ⊢ w ∈ B → z = B → w ∈ z
5 4 alrimiv ⊢ w ∈ B → ∀ z z = B → w ∈ z
6 eqid ⊢ B = B
7 eqeq1 ⊢ z = B → z = B ↔ B = B
8 7 3 imbi12d ⊢ z = B → z = B → w ∈ z ↔ B = B → w ∈ B
9 8 spcgv ⊢ B ∈ C → ∀ z z = B → w ∈ z → B = B → w ∈ B
10 6 9 mpii ⊢ B ∈ C → ∀ z z = B → w ∈ z → w ∈ B
11 5 10 impbid2 ⊢ B ∈ C → w ∈ B ↔ ∀ z z = B → w ∈ z
12 11 imim2i ⊢ x ∈ A → B ∈ C → x ∈ A → w ∈ B ↔ ∀ z z = B → w ∈ z
13 12 pm5.74d ⊢ x ∈ A → B ∈ C → x ∈ A → w ∈ B ↔ x ∈ A → ∀ z z = B → w ∈ z
14 13 alimi ⊢ ∀ x x ∈ A → B ∈ C → ∀ x x ∈ A → w ∈ B ↔ x ∈ A → ∀ z z = B → w ∈ z
15 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
16 14 15 syl ⊢ ∀ x x ∈ A → B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
17 2 16 sylbi ⊢ ∀ x ∈ A B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
18 df-ral ⊢ ∀ x ∈ A z = B → w ∈ z ↔ ∀ x x ∈ A → z = B → w ∈ z
19 18 albii ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ z ∀ x x ∈ A → z = B → w ∈ z
20 alcom ⊢ ∀ x ∀ z x ∈ A → z = B → w ∈ z ↔ ∀ z ∀ x x ∈ A → z = B → w ∈ z
21 19 20 bitr4i ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ x ∀ z x ∈ A → z = B → w ∈ z
22 r19.23v ⊢ ∀ x ∈ A z = B → w ∈ z ↔ ∃ x ∈ A z = B → w ∈ z
23 vex ⊢ z ∈ V
24 eqeq1 ⊢ y = z → y = B ↔ z = B
25 24 rexbidv ⊢ y = z → ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
26 23 25 elab ⊢ z ∈ y | ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
27 26 imbi1i ⊢ z ∈ y | ∃ x ∈ A y = B → w ∈ z ↔ ∃ x ∈ A z = B → w ∈ z
28 22 27 bitr4i ⊢ ∀ x ∈ A z = B → w ∈ z ↔ z ∈ y | ∃ x ∈ A y = B → w ∈ z
29 28 albii ⊢ ∀ z ∀ x ∈ A z = B → w ∈ z ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
30 19.21v ⊢ ∀ z x ∈ A → z = B → w ∈ z ↔ x ∈ A → ∀ z z = B → w ∈ z
31 30 albii ⊢ ∀ x ∀ z x ∈ A → z = B → w ∈ z ↔ ∀ x x ∈ A → ∀ z z = B → w ∈ z
32 21 29 31 3bitr3ri ⊢ ∀ x x ∈ A → ∀ z z = B → w ∈ z ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
33 17 32 bitrdi ⊢ ∀ x ∈ A B ∈ C → ∀ x x ∈ A → w ∈ B ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
34 1 33 bitrid ⊢ ∀ x ∈ A B ∈ C → ∀ x ∈ A w ∈ B ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
35 34 abbidv ⊢ ∀ x ∈ A B ∈ C → w | ∀ x ∈ A w ∈ B = w | ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
36 df-iin ⊢ ⋂ x ∈ A B = w | ∀ x ∈ A w ∈ B
37 df-int ⊢ ⋂ y | ∃ x ∈ A y = B = w | ∀ z z ∈ y | ∃ x ∈ A y = B → w ∈ z
38 35 36 37 3eqtr4g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B