Metamath Proof Explorer

Theorem dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Assertion dfiun2g 
|- ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ x A. x e. A B e. C
2 rspa 
 |-  ( ( A. x e. A B e. C /\ x e. A ) -> B e. C )
3 clel3g 
 |-  ( B e. C -> ( z e. B <-> E. y ( y = B /\ z e. y ) ) )
4 2 3 syl 
 |-  ( ( A. x e. A B e. C /\ x e. A ) -> ( z e. B <-> E. y ( y = B /\ z e. y ) ) )
5 1 4 rexbida 
 |-  ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. x e. A E. y ( y = B /\ z e. y ) ) )
6 rexcom4 
 |-  ( E. x e. A E. y ( y = B /\ z e. y ) <-> E. y E. x e. A ( y = B /\ z e. y ) )
7 5 6 syl6bb 
 |-  ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. y E. x e. A ( y = B /\ z e. y ) ) )
8 r19.41v 
 |-  ( E. x e. A ( y = B /\ z e. y ) <-> ( E. x e. A y = B /\ z e. y ) )
9 8 exbii 
 |-  ( E. y E. x e. A ( y = B /\ z e. y ) <-> E. y ( E. x e. A y = B /\ z e. y ) )
10 exancom 
 |-  ( E. y ( E. x e. A y = B /\ z e. y ) <-> E. y ( z e. y /\ E. x e. A y = B ) )
11 9 10 bitri 
 |-  ( E. y E. x e. A ( y = B /\ z e. y ) <-> E. y ( z e. y /\ E. x e. A y = B ) )
12 7 11 syl6bb 
 |-  ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. y ( z e. y /\ E. x e. A y = B ) ) )
13 eliun 
 |-  ( z e. U_ x e. A B <-> E. x e. A z e. B )
14 eluniab 
 |-  ( z e. U. { y | E. x e. A y = B } <-> E. y ( z e. y /\ E. x e. A y = B ) )
15 12 13 14 3bitr4g 
 |-  ( A. x e. A B e. C -> ( z e. U_ x e. A B <-> z e. U. { y | E. x e. A y = B } ) )
16 15 eqrdv 
 |-  ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )