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	alrimiv	|- ( ph -> A. x ( ps -> x e. A ) )
5		abss	|- ( { x | ps } C_ A <-> A. x ( ps -> x e. A ) )
6	4 5	sylibr	|- ( ph -> { x | ps } C_ A )
7	2 6	ssexd	|- ( ph -> { x | ps } e. _V )