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 
|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A w e. B <-> A. x ( x e. A -> w e. B ) )
2 df-ral 
 |-  ( A. x e. A B e. C <-> A. x ( x e. A -> B e. C ) )
3 eleq2 
 |-  ( z = B -> ( w e. z <-> w e. B ) )
4 3 biimprcd 
 |-  ( w e. B -> ( z = B -> w e. z ) )
5 4 alrimiv 
 |-  ( w e. B -> A. z ( z = B -> w e. z ) )
6 eqid 
 |-  B = B
7 eqeq1 
 |-  ( z = B -> ( z = B <-> B = B ) )
8 7 3 imbi12d 
 |-  ( z = B -> ( ( z = B -> w e. z ) <-> ( B = B -> w e. B ) ) )
9 8 spcgv 
 |-  ( B e. C -> ( A. z ( z = B -> w e. z ) -> ( B = B -> w e. B ) ) )
10 6 9 mpii 
 |-  ( B e. C -> ( A. z ( z = B -> w e. z ) -> w e. B ) )
11 5 10 impbid2 
 |-  ( B e. C -> ( w e. B <-> A. z ( z = B -> w e. z ) ) )
12 11 imim2i 
 |-  ( ( x e. A -> B e. C ) -> ( x e. A -> ( w e. B <-> A. z ( z = B -> w e. z ) ) ) )
13 12 pm5.74d 
 |-  ( ( x e. A -> B e. C ) -> ( ( x e. A -> w e. B ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
14 13 alimi 
 |-  ( A. x ( x e. A -> B e. C ) -> A. x ( ( x e. A -> w e. B ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
15 albi 
 |-  ( A. x ( ( x e. A -> w e. B ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) ) -> ( A. x ( x e. A -> w e. B ) <-> A. x ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
16 14 15 syl 
 |-  ( A. x ( x e. A -> B e. C ) -> ( A. x ( x e. A -> w e. B ) <-> A. x ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
17 2 16 sylbi 
 |-  ( A. x e. A B e. C -> ( A. x ( x e. A -> w e. B ) <-> A. x ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
18 df-ral 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> A. x ( x e. A -> ( z = B -> w e. z ) ) )
19 18 albii 
 |-  ( A. z A. x e. A ( z = B -> w e. z ) <-> A. z A. x ( x e. A -> ( z = B -> w e. z ) ) )
20 alcom 
 |-  ( A. x A. z ( x e. A -> ( z = B -> w e. z ) ) <-> A. z A. x ( x e. A -> ( z = B -> w e. z ) ) )
21 19 20 bitr4i 
 |-  ( A. z A. x e. A ( z = B -> w e. z ) <-> A. x A. z ( x e. A -> ( z = B -> w e. z ) ) )
22 r19.23v 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> ( E. x e. A z = B -> w e. z ) )
23 vex 
 |-  z e. _V
24 eqeq1 
 |-  ( y = z -> ( y = B <-> z = B ) )
25 24 rexbidv 
 |-  ( y = z -> ( E. x e. A y = B <-> E. x e. A z = B ) )
26 23 25 elab 
 |-  ( z e. { y | E. x e. A y = B } <-> E. x e. A z = B )
27 26 imbi1i 
 |-  ( ( z e. { y | E. x e. A y = B } -> w e. z ) <-> ( E. x e. A z = B -> w e. z ) )
28 22 27 bitr4i 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> ( z e. { y | E. x e. A y = B } -> w e. z ) )
29 28 albii 
 |-  ( A. z A. x e. A ( z = B -> w e. z ) <-> A. z ( z e. { y | E. x e. A y = B } -> w e. z ) )
30 19.21v 
 |-  ( A. z ( x e. A -> ( z = B -> w e. z ) ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) )
31 30 albii 
 |-  ( A. x A. z ( x e. A -> ( z = B -> w e. z ) ) <-> A. x ( x e. A -> A. z ( z = B -> w e. z ) ) )
32 21 29 31 3bitr3ri 
 |-  ( A. x ( x e. A -> A. z ( z = B -> w e. z ) ) <-> A. z ( z e. { y | E. x e. A y = B } -> w e. z ) )
33 17 32 bitrdi 
 |-  ( A. x e. A B e. C -> ( A. x ( x e. A -> w e. B ) <-> A. z ( z e. { y | E. x e. A y = B } -> w e. z ) ) )
34 1 33 bitrid 
 |-  ( A. x e. A B e. C -> ( A. x e. A w e. B <-> A. z ( z e. { y | E. x e. A y = B } -> w e. z ) ) )
35 34 abbidv 
 |-  ( A. x e. A B e. C -> { w | A. x e. A w e. B } = { w | A. z ( z e. { y | E. x e. A y = B } -> w e. z ) } )
36 df-iin 
 |-  |^|_ x e. A B = { w | A. x e. A w e. B }
37 df-int 
 |-  |^| { y | E. x e. A y = B } = { w | A. z ( z e. { y | E. x e. A y = B } -> w e. z ) }
38 35 36 37 3eqtr4g 
 |-  ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )