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

Metamath Proof Explorer

Theorem rabexd

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 . (Contributed by AV, 16-Jul-2019)

Ref Expression
Hypotheses rabexd.1 ⊢ B = x ∈ A | ψ
rabexd.2 ⊢ φ → A ∈ V
Assertion rabexd ⊢ φ → B ∈ V

Proof

Step Hyp Ref Expression
1 rabexd.1 ⊢ B = x ∈ A | ψ
2 rabexd.2 ⊢ φ → A ∈ V
3 rabexg ⊢ A ∈ V → x ∈ A | ψ ∈ V
4 2 3 syl ⊢ φ → x ∈ A | ψ ∈ V
5 1 4 eqeltrid ⊢ φ → B ∈ V