Theorem cnviun

Description: Converse of indexed union. (Contributed by RP, 20-Jun-2020)

	Ref	Expression
Assertion	cnviun	⊢ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡ 𝐵

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ ∪ 𝑥 ∈ 𝐴 𝐵
2		reliun	⊢ ( Rel ∪ 𝑥 ∈ 𝐴 ◡ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 Rel ◡ 𝐵 )
3		relcnv	⊢ Rel ◡ 𝐵
4	3	a1i	⊢ ( 𝑥 ∈ 𝐴 → Rel ◡ 𝐵 )
5	2 4	mprgbir	⊢ Rel ∪ 𝑥 ∈ 𝐴 ◡ 𝐵
6		vex	⊢ 𝑦 ∈ V
7		vex	⊢ 𝑧 ∈ V
8	6 7	opelcnv	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐵 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 )
9	8	bicomi	⊢ ( ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐵 )
10	9	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐵 )
11	6 7	opelcnv	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
12		eliun	⊢ ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 )
13	11 12	bitri	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 )
14		eliun	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ◡ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐵 )
15	10 13 14	3bitr4i	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ◡ 𝐵 )
16	1 5 15	eqrelriiv	⊢ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡ 𝐵