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	alrimiv	$$⊢\phi \to \forall x\left(\psi \to x\in A\right)$$
5		abss	$$⊢\left\{x|\psi \right\}\subseteq A\leftrightarrow \forall x\left(\psi \to x\in A\right)$$
6	4 5	sylibr	$$⊢\phi \to \left\{x|\psi \right\}\subseteq A$$
7	2 6	ssexd	$$⊢\phi \to \left\{x|\psi \right\}\in \mathrm{V}$$