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	⊢ ◡ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡ 𝑥

Proof

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	⊢ ◡ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡ 𝑥