Theorem rcompleq

Description: Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq . (Contributed by RP, 10-Jun-2021)

	Ref	Expression
Assertion	rcompleq	|- ( ( A C_ C /\ B C_ C ) -> ( A = B <-> ( C \ A ) = ( C \ B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( A C_ B /\ B C_ A ) <-> ( B C_ A /\ A C_ B ) )
2		sscon34b	|- ( ( B C_ C /\ A C_ C ) -> ( B C_ A <-> ( C \ A ) C_ ( C \ B ) ) )
3	2	ancoms	|- ( ( A C_ C /\ B C_ C ) -> ( B C_ A <-> ( C \ A ) C_ ( C \ B ) ) )
4		sscon34b	|- ( ( A C_ C /\ B C_ C ) -> ( A C_ B <-> ( C \ B ) C_ ( C \ A ) ) )
5	3 4	anbi12d	|- ( ( A C_ C /\ B C_ C ) -> ( ( B C_ A /\ A C_ B ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) ) )
6	1 5	bitrid	|- ( ( A C_ C /\ B C_ C ) -> ( ( A C_ B /\ B C_ A ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) ) )
7		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
8		eqss	|- ( ( C \ A ) = ( C \ B ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) )
9	6 7 8	3bitr4g	|- ( ( A C_ C /\ B C_ C ) -> ( A = B <-> ( C \ A ) = ( C \ B ) ) )