Theorem abrexex2g

Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	abrexex2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ 𝑊 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑧 ∃ 𝑥 ∈ 𝐴 𝜑
2		nfcv	⊢ Ⅎ 𝑦 𝐴
3		nfs1v	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
4	2 3	nfrex	⊢ Ⅎ 𝑦 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑
5		sbequ12	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
6	5	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 ) )
7	1 4 6	cbvabw	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 }
8		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
9	8	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 )
10	9	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑦 ∣ 𝜑 } } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 }
11	7 10	eqtr4i	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑦 ∣ 𝜑 } }
12		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑦 ∣ 𝜑 } }
13		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ 𝑊 ) → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ V )
14	12 13	eqeltrrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ 𝑊 ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑦 ∣ 𝜑 } } ∈ V )
15	11 14	eqeltrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ∈ 𝑊 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ∈ V )