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

Metamath Proof Explorer

Theorem abrexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x and y . See also abrexex . (Contributed by NM, 12-Sep-2004)

Ref Expression
Hypotheses abrexex2.1 ⊢ A ∈ V
abrexex2.2 ⊢ y | φ ∈ V
Assertion abrexex2 ⊢ y | ∃ x ∈ A φ ∈ V

Proof

Step Hyp Ref Expression
1 abrexex2.1 ⊢ A ∈ V
2 abrexex2.2 ⊢ y | φ ∈ V
3 2 rgenw ⊢ ∀ x ∈ A y | φ ∈ V
4 abrexex2g ⊢ A ∈ V ∧ ∀ x ∈ A y | φ ∈ V → y | ∃ x ∈ A φ ∈ V
5 1 3 4 mp2an ⊢ y | ∃ x ∈ A φ ∈ V