Theorem iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

	Ref	Expression
Assertion	iunab	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑦 𝐴
2		nfab1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
3	1 2	nfiun	⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 }
4		nfab1	⊢ Ⅎ 𝑦 { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }
5		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
6	5	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
7		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
8		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
9	6 7 8	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } )
10	3 4 9	eqri	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }