Metamath Proof Explorer

Theorem cnviun

Description: Converse of indexed union. (Contributed by RP, 20-Jun-2020)

Ref Expression
Assertion cnviun 
|- `' U_ x e. A B = U_ x e. A `' B

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' U_ x e. A B
2 reliun 
 |-  ( Rel U_ x e. A `' B <-> A. x e. A Rel `' B )
3 relcnv 
 |-  Rel `' B
4 3 a1i 
 |-  ( x e. A -> Rel `' B )
5 2 4 mprgbir 
 |-  Rel U_ x e. A `' B
6 vex 
 |-  y e. _V
7 vex 
 |-  z e. _V
8 6 7 opelcnv 
 |-  ( <. y , z >. e. `' B <-> <. z , y >. e. B )
9 8 bicomi 
 |-  ( <. z , y >. e. B <-> <. y , z >. e. `' B )
10 9 rexbii 
 |-  ( E. x e. A <. z , y >. e. B <-> E. x e. A <. y , z >. e. `' B )
11 6 7 opelcnv 
 |-  ( <. y , z >. e. `' U_ x e. A B <-> <. z , y >. e. U_ x e. A B )
12 eliun 
 |-  ( <. z , y >. e. U_ x e. A B <-> E. x e. A <. z , y >. e. B )
13 11 12 bitri 
 |-  ( <. y , z >. e. `' U_ x e. A B <-> E. x e. A <. z , y >. e. B )
14 eliun 
 |-  ( <. y , z >. e. U_ x e. A `' B <-> E. x e. A <. y , z >. e. `' B )
15 10 13 14 3bitr4i 
 |-  ( <. y , z >. e. `' U_ x e. A B <-> <. y , z >. e. U_ x e. A `' B )
16 1 5 15 eqrelriiv 
 |-  `' U_ x e. A B = U_ x e. A `' B