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

Metamath Proof Explorer

Theorem abexd

Description: Conditions for a class abstraction to be a set, deduction form. (Contributed by AV, 19-Apr-2025)

Ref Expression
Hypotheses abexd.1 ⊢ φ ∧ ψ → x ∈ A
abexd.2 ⊢ φ → A ∈ V
Assertion abexd ⊢ φ → x | ψ ∈ V

Proof

Step Hyp Ref Expression
1 abexd.1 ⊢ φ ∧ ψ → x ∈ A
2 abexd.2 ⊢ φ → A ∈ V
3 1 ex ⊢ φ → ψ → x ∈ A
4 3 abssdv ⊢ φ → x | ψ ⊆ A
5 2 4 ssexd ⊢ φ → x | ψ ∈ V