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 xABCxAB=y|xAy=B

Proof

Step Hyp Ref Expression
1 df-ral xAwBxxAwB
2 df-ral xABCxxABC
3 eleq2 z=BwzwB
4 3 biimprcd wBz=Bwz
5 4 alrimiv wBzz=Bwz
6 eqid B=B
7 eqeq1 z=Bz=BB=B
8 7 3 imbi12d z=Bz=BwzB=BwB
9 8 spcgv BCzz=BwzB=BwB
10 6 9 mpii BCzz=BwzwB
11 5 10 impbid2 BCwBzz=Bwz
12 11 imim2i xABCxAwBzz=Bwz
13 12 pm5.74d xABCxAwBxAzz=Bwz
14 13 alimi xxABCxxAwBxAzz=Bwz
15 albi xxAwBxAzz=BwzxxAwBxxAzz=Bwz
16 14 15 syl xxABCxxAwBxxAzz=Bwz
17 2 16 sylbi xABCxxAwBxxAzz=Bwz
18 df-ral xAz=BwzxxAz=Bwz
19 18 albii zxAz=BwzzxxAz=Bwz
20 alcom xzxAz=BwzzxxAz=Bwz
21 19 20 bitr4i zxAz=BwzxzxAz=Bwz
22 r19.23v xAz=BwzxAz=Bwz
23 vex zV
24 eqeq1 y=zy=Bz=B
25 24 rexbidv y=zxAy=BxAz=B
26 23 25 elab zy|xAy=BxAz=B
27 26 imbi1i zy|xAy=BwzxAz=Bwz
28 22 27 bitr4i xAz=Bwzzy|xAy=Bwz
29 28 albii zxAz=Bwzzzy|xAy=Bwz
30 19.21v zxAz=BwzxAzz=Bwz
31 30 albii xzxAz=BwzxxAzz=Bwz
32 21 29 31 3bitr3ri xxAzz=Bwzzzy|xAy=Bwz
33 17 32 bitrdi xABCxxAwBzzy|xAy=Bwz
34 1 33 bitrid xABCxAwBzzy|xAy=Bwz
35 34 abbidv xABCw|xAwB=w|zzy|xAy=Bwz
36 df-iin xAB=w|xAwB
37 df-int y|xAy=B=w|zzy|xAy=Bwz
38 35 36 37 3eqtr4g xABCxAB=y|xAy=B