ssdifsym

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

		Ref	Expression
	Assertion	ssdifsym	$⊢ (A \subseteq V \land B \subseteq V) \to (B = V ∖ A \leftrightarrow A = V ∖ B)$

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

Metamath Proof Explorer