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 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 )