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=⋃x∈Ax-1

Proof

Step Hyp Ref Expression
1 elcnv2 ⊢y∈⋃A-1↔∃z∃wy=zw∧wz∈⋃A
2 eluni2 ⊢wz∈⋃A↔∃x∈Awz∈x
3 2 anbi2i ⊢y=zw∧wz∈⋃A↔y=zw∧∃x∈Awz∈x
4 r19.42v ⊢∃x∈Ay=zw∧wz∈x↔y=zw∧∃x∈Awz∈x
5 3 4 bitr4i ⊢y=zw∧wz∈⋃A↔∃x∈Ay=zw∧wz∈x
6 5 2exbii ⊢∃z∃wy=zw∧wz∈⋃A↔∃z∃w∃x∈Ay=zw∧wz∈x
7 elcnv2 ⊢y∈x-1↔∃z∃wy=zw∧wz∈x
8 7 rexbii ⊢∃x∈Ay∈x-1↔∃x∈A∃z∃wy=zw∧wz∈x
9 rexcom4 ⊢∃x∈A∃z∃wy=zw∧wz∈x↔∃z∃x∈A∃wy=zw∧wz∈x
10 rexcom4 ⊢∃x∈A∃wy=zw∧wz∈x↔∃w∃x∈Ay=zw∧wz∈x
11 10 exbii ⊢∃z∃x∈A∃wy=zw∧wz∈x↔∃z∃w∃x∈Ay=zw∧wz∈x
12 8 9 11 3bitrri ⊢∃z∃w∃x∈Ay=zw∧wz∈x↔∃x∈Ay∈x-1
13 1 6 12 3bitri ⊢y∈⋃A-1↔∃x∈Ay∈x-1
14 eliun ⊢y∈⋃x∈Ax-1↔∃x∈Ay∈x-1
15 13 14 bitr4i ⊢y∈⋃A-1↔y∈⋃x∈Ax-1
16 15 eqriv ⊢⋃A-1=⋃x∈Ax-1