This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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		ssdifim	$⊢ (B \subseteq V \land A = V ∖ B) \to B = V ∖ A$
4	3	ex	$⊢ B \subseteq V \to (A = V ∖ B \to B = V ∖ A)$
5	2 4	anbiim	$⊢ (A \subseteq V \land B \subseteq V) \to (B = V ∖ A \leftrightarrow A = V ∖ B)$