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	$$⊢\left(\phi \wedge \psi \right)\to x\in A$$
	abexd.2	$$⊢\phi \to A\in V$$
Assertion	abexd	$$⊢\phi \to \left\{x|\psi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		abexd.1	$$⊢\left(\phi \wedge \psi \right)\to x\in A$$
2		abexd.2	$$⊢\phi \to A\in V$$
3	1	ex	$$⊢\phi \to \left(\psi \to x\in A\right)$$
4	3	abssdv	$$⊢\phi \to \left\{x|\psi \right\}\subseteq A$$
5	2 4	ssexd	$$⊢\phi \to \left\{x|\psi \right\}\in \mathrm{V}$$