Metamath Proof Explorer


Theorem cnviun

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

Ref Expression
Assertion cnviun xAB-1=xAB-1

Proof

Step Hyp Ref Expression
1 relcnv RelxAB-1
2 reliun RelxAB-1xARelB-1
3 relcnv RelB-1
4 3 a1i xARelB-1
5 2 4 mprgbir RelxAB-1
6 vex yV
7 vex zV
8 6 7 opelcnv yzB-1zyB
9 8 bicomi zyByzB-1
10 9 rexbii xAzyBxAyzB-1
11 6 7 opelcnv yzxAB-1zyxAB
12 eliun zyxABxAzyB
13 11 12 bitri yzxAB-1xAzyB
14 eliun yzxAB-1xAyzB-1
15 10 13 14 3bitr4i yzxAB-1yzxAB-1
16 1 5 15 eqrelriiv xAB-1=xAB-1