This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 nfrexw ⊢ Ⅎ 𝑦 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑
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 )