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

Metamath Proof Explorer

Theorem rabexgfGS

Description: Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017)

Ref Expression
Hypothesis rabexgfGS.1 ⊢ Ⅎ _ x A
Assertion rabexgfGS ⊢ A ∈ V → x ∈ A | φ ∈ V

Proof

Step Hyp Ref Expression
1 rabexgfGS.1 ⊢ Ⅎ _ x A
2 nfrab1 ⊢ Ⅎ _ x x ∈ A | φ
3 2 1 dfssf ⊢ x ∈ A | φ ⊆ A ↔ ∀ x x ∈ x ∈ A | φ → x ∈ A
4 rabidim1 ⊢ x ∈ x ∈ A | φ → x ∈ A
5 3 4 mpgbir ⊢ x ∈ A | φ ⊆ A
6 elex ⊢ A ∈ V → A ∈ V
7 ssexg ⊢ x ∈ A | φ ⊆ A ∧ A ∈ V → x ∈ A | φ ∈ V
8 5 6 7 sylancr ⊢ A ∈ V → x ∈ A | φ ∈ V