Theorem brrpssg

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

	Ref	Expression
Assertion	brrpssg	$$⊢B\in V\to \left(A[\subset ]B\leftrightarrow A\subset B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢B\in V\to B\in \mathrm{V}$$
2		relrpss	$$⊢\mathrm{Rel}[\subset ]$$
3	2	brrelex1i	$$⊢A[\subset ]B\to A\in \mathrm{V}$$
4	1 3	anim12i	$$⊢\left(B\in V\wedge A[\subset ]B\right)\to \left(B\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$
5	1	adantr	$$⊢\left(B\in V\wedge A\subset B\right)\to B\in \mathrm{V}$$
6		pssss	$$⊢A\subset B\to A\subseteq B$$
7		ssexg	$$⊢\left(A\subseteq B\wedge B\in \mathrm{V}\right)\to A\in \mathrm{V}$$
8	6 1 7	syl2anr	$$⊢\left(B\in V\wedge A\subset B\right)\to A\in \mathrm{V}$$
9	5 8	jca	$$⊢\left(B\in V\wedge A\subset B\right)\to \left(B\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$
10		psseq1	$$⊢x=A\to \left(x\subset y\leftrightarrow A\subset y\right)$$
11		psseq2	$$⊢y=B\to \left(A\subset y\leftrightarrow A\subset B\right)$$
12		df-rpss	$$⊢[\subset ]=\left\{⟨x,y⟩|x\subset y\right\}$$
13	10 11 12	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A[\subset ]B\leftrightarrow A\subset B\right)$$
14	13	ancoms	$$⊢\left(B\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(A[\subset ]B\leftrightarrow A\subset B\right)$$
15	4 9 14	pm5.21nd	$$⊢B\in V\to \left(A[\subset ]B\leftrightarrow A\subset B\right)$$