Theorem brrpss

Description: The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypothesis	brrpss.a	$$⊢B\in \mathrm{V}$$
Assertion	brrpss	$$⊢A[\subset ]B\leftrightarrow A\subset B$$

Proof

Step	Hyp	Ref	Expression
1		brrpss.a	$$⊢B\in \mathrm{V}$$
2		brrpssg	$$⊢B\in \mathrm{V}\to \left(A[\subset ]B\leftrightarrow A\subset B\right)$$
3	1 2	ax-mp	$$⊢A[\subset ]B\leftrightarrow A\subset B$$