Theorem dfiunv2

Description: Define double indexed union. (Contributed by FL, 6-Nov-2013)

	Ref	Expression
Assertion	dfiunv2	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 }
2	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } )
3	2	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐴 { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 }
4		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } }
5		vex	⊢ 𝑧 ∈ V
6		eleq1w	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶 ) )
7	6	rexbidv	⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 ) )
8	5 7	elab	⊢ ( 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
9	8	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
10	9	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }
11	3 4 10	3eqtri	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }