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\cap V\subseteq V\setminus B\leftrightarrow B\cap V\subseteq V\setminus A$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢A\cap B=B\cap A$$
2	1	ineq1i	$$⊢\left(A\cap B\right)\cap V=\left(B\cap A\right)\cap V$$
3	2	eqeq1i	$$⊢\left(A\cap B\right)\cap V=\varnothing \leftrightarrow \left(B\cap A\right)\cap V=\varnothing$$
4		bj-disj2r	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow \left(A\cap B\right)\cap V=\varnothing$$
5		bj-disj2r	$$⊢B\cap V\subseteq V\setminus A\leftrightarrow \left(B\cap A\right)\cap V=\varnothing$$
6	3 4 5	3bitr4i	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow B\cap V\subseteq V\setminus A$$