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 syl5bb 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