Theorem sssseq

Description: If a class is a subclass of another class, then the classes are equal if and only if the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020)

	Ref	Expression
Assertion	sssseq	|- ( B C_ A -> ( A C_ B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
2	1	rbaibr	|- ( B C_ A -> ( A C_ B <-> A = B ) )