Metamath Proof Explorer

Theorem iinabrex

Description: Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024)

Ref Expression
Assertion iinabrex ⊢ ∀ x ∈ A B ∈ V → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ x ∀ x ∈ A t ∈ B
2 nfv ⊢ Ⅎ x t ∈ z
3 eleq2 ⊢ z = B → t ∈ z ↔ t ∈ B
4 vex ⊢ z ∈ V
5 4 a1i ⊢ ∀ x ∈ A t ∈ B → z ∈ V
6 rspa ⊢ ∀ x ∈ A t ∈ B ∧ x ∈ A → t ∈ B
7 1 2 3 5 6 elabreximd ⊢ ∀ x ∈ A t ∈ B ∧ z ∈ y | ∃ x ∈ A y = B → t ∈ z
8 7 ex ⊢ ∀ x ∈ A t ∈ B → z ∈ y | ∃ x ∈ A y = B → t ∈ z
9 8 alrimiv ⊢ ∀ x ∈ A t ∈ B → ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
10 9 adantl ⊢ ∀ x ∈ A B ∈ V ∧ ∀ x ∈ A t ∈ B → ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
11 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ∈ V
12 2 nfci ⊢ Ⅎ _ x z
13 nfre1 ⊢ Ⅎ x ∃ x ∈ A y = B
14 13 nfab ⊢ Ⅎ _ x y | ∃ x ∈ A y = B
15 12 14 nfel ⊢ Ⅎ x z ∈ y | ∃ x ∈ A y = B
16 15 2 nfim ⊢ Ⅎ x z ∈ y | ∃ x ∈ A y = B → t ∈ z
17 16 nfal ⊢ Ⅎ x ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
18 11 17 nfan ⊢ Ⅎ x ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
19 rspa ⊢ ∀ x ∈ A B ∈ V ∧ x ∈ A → B ∈ V
20 19 elexd ⊢ ∀ x ∈ A B ∈ V ∧ x ∈ A → B ∈ V
21 20 adantlr ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ x ∈ A → B ∈ V
22 simplr ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ x ∈ A → ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
23 rspe ⊢ x ∈ A ∧ y = B → ∃ x ∈ A y = B
24 tbtru ⊢ ∃ x ∈ A y = B ↔ ∃ x ∈ A y = B ↔ ⊤
25 23 24 sylib ⊢ x ∈ A ∧ y = B → ∃ x ∈ A y = B ↔ ⊤
26 25 ex ⊢ x ∈ A → y = B → ∃ x ∈ A y = B ↔ ⊤
27 26 alrimiv ⊢ x ∈ A → ∀ y y = B → ∃ x ∈ A y = B ↔ ⊤
28 27 adantl ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ x ∈ A → ∀ y y = B → ∃ x ∈ A y = B ↔ ⊤
29 elabgt ⊢ B ∈ V ∧ ∀ y y = B → ∃ x ∈ A y = B ↔ ⊤ → B ∈ y | ∃ x ∈ A y = B ↔ ⊤
30 tbtru ⊢ B ∈ y | ∃ x ∈ A y = B ↔ B ∈ y | ∃ x ∈ A y = B ↔ ⊤
31 29 30 sylibr ⊢ B ∈ V ∧ ∀ y y = B → ∃ x ∈ A y = B ↔ ⊤ → B ∈ y | ∃ x ∈ A y = B
32 21 28 31 syl2anc ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ x ∈ A → B ∈ y | ∃ x ∈ A y = B
33 eleq1 ⊢ z = B → z ∈ y | ∃ x ∈ A y = B ↔ B ∈ y | ∃ x ∈ A y = B
34 33 3 imbi12d ⊢ z = B → z ∈ y | ∃ x ∈ A y = B → t ∈ z ↔ B ∈ y | ∃ x ∈ A y = B → t ∈ B
35 34 spcgv ⊢ B ∈ V → ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z → B ∈ y | ∃ x ∈ A y = B → t ∈ B
36 35 imp ⊢ B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z → B ∈ y | ∃ x ∈ A y = B → t ∈ B
37 36 imp ⊢ B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ B ∈ y | ∃ x ∈ A y = B → t ∈ B
38 21 22 32 37 syl21anc ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z ∧ x ∈ A → t ∈ B
39 38 ex ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z → x ∈ A → t ∈ B
40 18 39 ralrimi ⊢ ∀ x ∈ A B ∈ V ∧ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z → ∀ x ∈ A t ∈ B
41 10 40 impbida ⊢ ∀ x ∈ A B ∈ V → ∀ x ∈ A t ∈ B ↔ ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
42 41 abbidv ⊢ ∀ x ∈ A B ∈ V → t | ∀ x ∈ A t ∈ B = t | ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
43 df-iin ⊢ ⋂ x ∈ A B = t | ∀ x ∈ A t ∈ B
44 43 a1i ⊢ ∀ x ∈ A B ∈ V → ⋂ x ∈ A B = t | ∀ x ∈ A t ∈ B
45 df-int ⊢ ⋂ y | ∃ x ∈ A y = B = t | ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
46 45 a1i ⊢ ∀ x ∈ A B ∈ V → ⋂ y | ∃ x ∈ A y = B = t | ∀ z z ∈ y | ∃ x ∈ A y = B → t ∈ z
47 42 44 46 3eqtr4d ⊢ ∀ x ∈ A B ∈ V → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B