Theorem brssr

Description: The subset relation and subclass relationship ( df-ss ) are the same, that is, ( AS B <-> A C B ) when B is a set. (Contributed by Peter Mazsa, 31-Jul-2019)

	Ref	Expression
Assertion	brssr	|- ( B e. V -> ( A _S B <-> A C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		relssr	|- Rel _S
2	1	brrelex1i	|- ( A _S B -> A e. _V )
3	2	adantl	|- ( ( B e. V /\ A _S B ) -> A e. _V )
4		simpl	|- ( ( B e. V /\ A _S B ) -> B e. V )
5	3 4	jca	|- ( ( B e. V /\ A _S B ) -> ( A e. _V /\ B e. V ) )
6		ssexg	|- ( ( A C_ B /\ B e. V ) -> A e. _V )
7		simpr	|- ( ( A C_ B /\ B e. V ) -> B e. V )
8	6 7	jca	|- ( ( A C_ B /\ B e. V ) -> ( A e. _V /\ B e. V ) )
9	8	ancoms	|- ( ( B e. V /\ A C_ B ) -> ( A e. _V /\ B e. V ) )
10		sseq1	|- ( x = A -> ( x C_ y <-> A C_ y ) )
11		sseq2	|- ( y = B -> ( A C_ y <-> A C_ B ) )
12		df-ssr	|- _S = { <. x , y >. | x C_ y }
13	10 11 12	brabg	|- ( ( A e. _V /\ B e. V ) -> ( A _S B <-> A C_ B ) )
14	5 9 13	pm5.21nd	|- ( B e. V -> ( A _S B <-> A C_ B ) )