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 ⊢ A ∈ V ∧ ∀ x ∈ A y | φ ∈ W → y | ∃ x ∈ A φ ∈ V

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ z ∃ x ∈ A φ
2 nfcv ⊢ Ⅎ _ y A
3 nfs1v ⊢ Ⅎ y z y φ
4 2 3 nfrexw ⊢ Ⅎ y ∃ x ∈ A z y φ
5 sbequ12 ⊢ y = z → φ ↔ z y φ
6 5 rexbidv ⊢ y = z → ∃ x ∈ A φ ↔ ∃ x ∈ A z y φ
7 1 4 6 cbvabw ⊢ y | ∃ x ∈ A φ = z | ∃ x ∈ A z y φ
8 df-clab ⊢ z ∈ y | φ ↔ z y φ
9 8 rexbii ⊢ ∃ x ∈ A z ∈ y | φ ↔ ∃ x ∈ A z y φ
10 9 abbii ⊢ z | ∃ x ∈ A z ∈ y | φ = z | ∃ x ∈ A z y φ
11 7 10 eqtr4i ⊢ y | ∃ x ∈ A φ = z | ∃ x ∈ A z ∈ y | φ
12 df-iun ⊢ ⋃ x ∈ A y | φ = z | ∃ x ∈ A z ∈ y | φ
13 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A y | φ ∈ W → ⋃ x ∈ A y | φ ∈ V
14 12 13 eqeltrrid ⊢ A ∈ V ∧ ∀ x ∈ A y | φ ∈ W → z | ∃ x ∈ A z ∈ y | φ ∈ V
15 11 14 eqeltrid ⊢ A ∈ V ∧ ∀ x ∈ A y | φ ∈ W → y | ∃ x ∈ A φ ∈ V