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 clel4g 
 |-  ( B e. C -> ( w e. B <-> A. z ( z = B -> w e. z ) ) )
4 3 imim2i 
 |-  ( ( x e. A -> B e. C ) -> ( x e. A -> ( w e. B <-> A. z ( z = B -> w e. z ) ) ) )
5 4 pm5.74d 
 |-  ( ( x e. A -> B e. C ) -> ( ( x e. A -> w e. B ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) ) )
6 5 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 ) ) ) )
7 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 ) ) ) )
8 6 7 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 ) ) ) )
9 2 8 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 ) ) ) )
10 df-ral 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> A. x ( x e. A -> ( z = B -> w e. z ) ) )
11 10 albii 
 |-  ( A. z A. x e. A ( z = B -> w e. z ) <-> A. z A. x ( x e. A -> ( z = B -> w e. z ) ) )
12 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 ) ) )
13 11 12 bitr4i 
 |-  ( A. z A. x e. A ( z = B -> w e. z ) <-> A. x A. z ( x e. A -> ( z = B -> w e. z ) ) )
14 r19.23v 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> ( E. x e. A z = B -> w e. z ) )
15 vex 
 |-  z e. _V
16 eqeq1 
 |-  ( y = z -> ( y = B <-> z = B ) )
17 16 rexbidv 
 |-  ( y = z -> ( E. x e. A y = B <-> E. x e. A z = B ) )
18 15 17 elab 
 |-  ( z e. { y | E. x e. A y = B } <-> E. x e. A z = B )
19 18 imbi1i 
 |-  ( ( z e. { y | E. x e. A y = B } -> w e. z ) <-> ( E. x e. A z = B -> w e. z ) )
20 14 19 bitr4i 
 |-  ( A. x e. A ( z = B -> w e. z ) <-> ( z e. { y | E. x e. A y = B } -> w e. z ) )
21 20 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 ) )
22 19.21v 
 |-  ( A. z ( x e. A -> ( z = B -> w e. z ) ) <-> ( x e. A -> A. z ( z = B -> w e. z ) ) )
23 22 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 ) ) )
24 13 21 23 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 ) )
25 9 24 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 ) ) )
26 1 25 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 ) ) )
27 26 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 ) } )
28 df-iin 
 |-  |^|_ x e. A B = { w | A. x e. A w e. B }
29 df-int 
 |-  |^| { y | E. x e. A y = B } = { w | A. z ( z e. { y | E. x e. A y = B } -> w e. z ) }
30 27 28 29 3eqtr4g 
 |-  ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )