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 
|- ( ( ph /\ ps ) -> x e. A )
abexd.2 
|- ( ph -> A e. V )
Assertion abexd 
|- ( ph -> { x | ps } e. _V )

Proof

Step Hyp Ref Expression
1 abexd.1 
 |-  ( ( ph /\ ps ) -> x e. A )
2 abexd.2 
 |-  ( ph -> A e. V )
3 1 ex 
 |-  ( ph -> ( ps -> x e. A ) )
4 3 abssdv 
 |-  ( ph -> { x | ps } C_ A )
5 2 4 ssexd 
 |-  ( ph -> { x | ps } e. _V )