Theorem ssdifsym

Description: Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022)

	Ref	Expression
Assertion	ssdifsym	$$⊢\left(A\subseteq V\wedge B\subseteq V\right)\to \left(B=V\setminus A\leftrightarrow A=V\setminus B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssdifim	$$⊢\left(A\subseteq V\wedge B=V\setminus A\right)\to A=V\setminus B$$
2	1	ex	$$⊢A\subseteq V\to \left(B=V\setminus A\to A=V\setminus B\right)$$
3	2	adantr	$$⊢\left(A\subseteq V\wedge B\subseteq V\right)\to \left(B=V\setminus A\to A=V\setminus B\right)$$
4		ssdifim	$$⊢\left(B\subseteq V\wedge A=V\setminus B\right)\to B=V\setminus A$$
5	4	ex	$$⊢B\subseteq V\to \left(A=V\setminus B\to B=V\setminus A\right)$$
6	5	adantl	$$⊢\left(A\subseteq V\wedge B\subseteq V\right)\to \left(A=V\setminus B\to B=V\setminus A\right)$$
7	3 6	impbid	$$⊢\left(A\subseteq V\wedge B\subseteq V\right)\to \left(B=V\setminus A\leftrightarrow A=V\setminus B\right)$$