Description: Converse of indexed union. (Contributed by RP, 20-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | cnviun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |
|
2 | reliun | |
|
3 | relcnv | |
|
4 | 3 | a1i | |
5 | 2 4 | mprgbir | |
6 | vex | |
|
7 | vex | |
|
8 | 6 7 | opelcnv | |
9 | 8 | bicomi | |
10 | 9 | rexbii | |
11 | 6 7 | opelcnv | |
12 | eliun | |
|
13 | 11 12 | bitri | |
14 | eliun | |
|
15 | 10 13 14 | 3bitr4i | |
16 | 1 5 15 | eqrelriiv | |