Theorem bj-projex

Description: Sethood of the class projection. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-projex	$$⊢B\in V\to \left(AProjB\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-proj	$$⊢\left(AProjB\right)=\left\{x|\left\{x\right\}\in B\left[\left\{A\right\}\right]\right\}$$
2		bj-clex	$$⊢B\in V\to \left\{x|\left\{x\right\}\in B\left[\left\{A\right\}\right]\right\}\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢B\in V\to \left(AProjB\right)\in \mathrm{V}$$