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 e. V -> ( A [C.] B <-> A C. B ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( B e. V -> B e. _V )
2		relrpss	|- Rel [C.]
3	2	brrelex1i	|- ( A [C.] B -> A e. _V )
4	1 3	anim12i	|- ( ( B e. V /\ A [C.] B ) -> ( B e. _V /\ A e. _V ) )
5	1	adantr	|- ( ( B e. V /\ A C. B ) -> B e. _V )
6		pssss	|- ( A C. B -> A C_ B )
7		ssexg	|- ( ( A C_ B /\ B e. _V ) -> A e. _V )
8	6 1 7	syl2anr	|- ( ( B e. V /\ A C. B ) -> A e. _V )
9	5 8	jca	|- ( ( B e. V /\ A C. B ) -> ( B e. _V /\ A e. _V ) )
10		psseq1	|- ( x = A -> ( x C. y <-> A C. y ) )
11		psseq2	|- ( y = B -> ( A C. y <-> A C. B ) )
12		df-rpss	|- [C.] = { <. x , y >. | x C. y }
13	10 11 12	brabg	|- ( ( A e. _V /\ B e. _V ) -> ( A [C.] B <-> A C. B ) )
14	13	ancoms	|- ( ( B e. _V /\ A e. _V ) -> ( A [C.] B <-> A C. B ) )
15	4 9 14	pm5.21nd	|- ( B e. V -> ( A [C.] B <-> A C. B ) )