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	3 4	cleqf	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ) )
6		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
7	6	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
8		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
9		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
10	7 8 9	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } )
11	5 10	mpgbir	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }