Description: Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | dfiin2g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral | |
|
2 | df-ral | |
|
3 | eleq2 | |
|
4 | 3 | biimprcd | |
5 | 4 | alrimiv | |
6 | eqid | |
|
7 | eqeq1 | |
|
8 | 7 3 | imbi12d | |
9 | 8 | spcgv | |
10 | 6 9 | mpii | |
11 | 5 10 | impbid2 | |
12 | 11 | imim2i | |
13 | 12 | pm5.74d | |
14 | 13 | alimi | |
15 | albi | |
|
16 | 14 15 | syl | |
17 | 2 16 | sylbi | |
18 | df-ral | |
|
19 | 18 | albii | |
20 | alcom | |
|
21 | 19 20 | bitr4i | |
22 | r19.23v | |
|
23 | vex | |
|
24 | eqeq1 | |
|
25 | 24 | rexbidv | |
26 | 23 25 | elab | |
27 | 26 | imbi1i | |
28 | 22 27 | bitr4i | |
29 | 28 | albii | |
30 | 19.21v | |
|
31 | 30 | albii | |
32 | 21 29 31 | 3bitr3ri | |
33 | 17 32 | bitrdi | |
34 | 1 33 | bitrid | |
35 | 34 | abbidv | |
36 | df-iin | |
|
37 | df-int | |
|
38 | 35 36 37 | 3eqtr4g | |