Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

	Ref	Expression
Assertion	iuncom4	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
2	1	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
3		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
4	2 3	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
5		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
6	5	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) ↔ ∃ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
7	4 6	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
8		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐵 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 )
9	8	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 )
10		df-rex	⊢ ( ∃ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
11		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
12	11	anbi1i	⊢ ( ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
13	12	exbii	⊢ ( ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧 ) ↔ ∃ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
14	10 13	bitri	⊢ ( ∃ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ 𝑧 ↔ ∃ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧 ) )
15	7 9 14	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ∪ 𝐵 ↔ ∃ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ 𝑧 )
16		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ∪ 𝐵 )
17		eluni2	⊢ ( 𝑦 ∈ ∪ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ 𝑧 )
18	15 16 17	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 ↔ 𝑦 ∈ ∪ ∪ 𝑥 ∈ 𝐴 𝐵 )
19	18	eqriv	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵