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∈AB∈V→⋂x∈AB=⋂y|∃x∈Ay=B

Proof

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