Description: The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elcnv2 | |
|
2 | eluni2 | |
|
3 | 2 | anbi2i | |
4 | r19.42v | |
|
5 | 3 4 | bitr4i | |
6 | 5 | 2exbii | |
7 | elcnv2 | |
|
8 | 7 | rexbii | |
9 | rexcom4 | |
|
10 | rexcom4 | |
|
11 | 10 | exbii | |
12 | 8 9 11 | 3bitrri | |
13 | 1 6 12 | 3bitri | |
14 | eliun | |
|
15 | 13 14 | bitr4i | |
16 | 15 | eqriv | |