Metamath Proof Explorer


Theorem cnvuni

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 A-1=xAx-1

Proof

Step Hyp Ref Expression
1 elcnv2 yA-1zwy=zwwzA
2 eluni2 wzAxAwzx
3 2 anbi2i y=zwwzAy=zwxAwzx
4 r19.42v xAy=zwwzxy=zwxAwzx
5 3 4 bitr4i y=zwwzAxAy=zwwzx
6 5 2exbii zwy=zwwzAzwxAy=zwwzx
7 elcnv2 yx-1zwy=zwwzx
8 7 rexbii xAyx-1xAzwy=zwwzx
9 rexcom4 xAzwy=zwwzxzxAwy=zwwzx
10 rexcom4 xAwy=zwwzxwxAy=zwwzx
11 10 exbii zxAwy=zwwzxzwxAy=zwwzx
12 8 9 11 3bitrri zwxAy=zwwzxxAyx-1
13 1 6 12 3bitri yA-1xAyx-1
14 eliun yxAx-1xAyx-1
15 13 14 bitr4i yA-1yxAx-1
16 15 eqriv A-1=xAx-1