Theorem prcssprc

Description: The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Assertion	prcssprc	$$⊢\left(A\subseteq B\wedge A\notin \mathrm{V}\right)\to B\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssexg	$$⊢\left(A\subseteq B\wedge B\in \mathrm{V}\right)\to A\in \mathrm{V}$$
2	1	ex	$$⊢A\subseteq B\to \left(B\in \mathrm{V}\to A\in \mathrm{V}\right)$$
3	2	nelcon3d	$$⊢A\subseteq B\to \left(A\notin \mathrm{V}\to B\notin \mathrm{V}\right)$$
4	3	imp	$$⊢\left(A\subseteq B\wedge A\notin \mathrm{V}\right)\to B\notin \mathrm{V}$$