Theorem bj-sscon

Description: Contraposition law for relative subclasses. Relative and generalized version of ssconb , which it can shorten, as well as conss2 . (Contributed by BJ, 11-Nov-2021) This proof does not rely, even indirectly, on ssconb nor conss2 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-sscon	|- ( ( A i^i V ) C_ ( V \ B ) <-> ( B i^i V ) C_ ( V \ A ) )

Proof

Step	Hyp	Ref	Expression
1		incom	|- ( A i^i B ) = ( B i^i A )
2	1	ineq1i	|- ( ( A i^i B ) i^i V ) = ( ( B i^i A ) i^i V )
3	2	eqeq1i	|- ( ( ( A i^i B ) i^i V ) = (/) <-> ( ( B i^i A ) i^i V ) = (/) )
4		bj-disj2r	|- ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i B ) i^i V ) = (/) )
5		bj-disj2r	|- ( ( B i^i V ) C_ ( V \ A ) <-> ( ( B i^i A ) i^i V ) = (/) )
6	3 4 5	3bitr4i	|- ( ( A i^i V ) C_ ( V \ B ) <-> ( B i^i V ) C_ ( V \ A ) )