Theorem rabex2

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	rabex2.1	$$⊢B=\left\{x\in A|\psi \right\}$$
	rabex2.2	$$⊢A\in \mathrm{V}$$
Assertion	rabex2	$$⊢B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rabex2.1	$$⊢B=\left\{x\in A|\psi \right\}$$
2		rabex2.2	$$⊢A\in \mathrm{V}$$
3		id	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
4	1 3	rabexd	$$⊢A\in \mathrm{V}\to B\in \mathrm{V}$$
5	2 4	ax-mp	$$⊢B\in \mathrm{V}$$