Theorem bj-clex

Description: Sethood of certain classes. (Contributed by BJ, 2-Apr-2019)

	Ref	Expression
Assertion	bj-clex	$$⊢A\in V\to \left\{x|\left\{x\right\}\in A\left[B\right]\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		imaexg	$$⊢A\in V\to A\left[B\right]\in \mathrm{V}$$
2		bj-snsetex	$$⊢A\left[B\right]\in \mathrm{V}\to \left\{x|\left\{x\right\}\in A\left[B\right]\right\}\in \mathrm{V}$$
3	1 2	syl	$$⊢A\in V\to \left\{x|\left\{x\right\}\in A\left[B\right]\right\}\in \mathrm{V}$$