Theorem rabiun

Description: Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017)

	Ref	Expression
Assertion	rabiun	⊢ { 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑 } = ∪ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		eliun	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 )
2	1	anbi1i	⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
3		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
4	2 3	bitr4i	⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
5	4	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
6		df-rab	⊢ { 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝜑 ) }
7		iunab	⊢ ∪ 𝑦 ∈ 𝐴 { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
8	5 6 7	3eqtr4i	⊢ { 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑 } = ∪ 𝑦 ∈ 𝐴 { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
9		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
10	9	a1i	⊢ ( 𝑦 ∈ 𝐴 → { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
11	10	iuneq2i	⊢ ∪ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ∪ 𝑦 ∈ 𝐴 { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
12	8 11	eqtr4i	⊢ { 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑 } = ∪ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝜑 }