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 ∈ A x -1

Proof

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