compsscnvlem

		Ref	Expression
	Assertion	compsscnvlem	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to (y \in 𝒫 A \land x = A ∖ y)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to y = A ∖ x$
2		difss	$⊢ A ∖ x \subseteq A$
3	1 2	eqsstrdi	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to y \subseteq A$
4		velpw	$⊢ y \in 𝒫 A \leftrightarrow y \subseteq A$
5	3 4	sylibr	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to y \in 𝒫 A$
6	1	difeq2d	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to A ∖ y = A ∖ (A ∖ x)$
7		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
8	7	adantr	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to x \subseteq A$
9		dfss4	$⊢ x \subseteq A \leftrightarrow A ∖ (A ∖ x) = x$
10	8 9	sylib	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to A ∖ (A ∖ x) = x$
11	6 10	eqtr2d	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to x = A ∖ y$
12	5 11	jca	$⊢ (x \in 𝒫 A \land y = A ∖ x) \to (y \in 𝒫 A \land x = A ∖ y)$

Metamath Proof Explorer