# Metamath Proof Explorer

## Theorem compsscnvlem

Description: Lemma for compsscnv . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion compsscnvlem ${⊢}\left({x}\in 𝒫{A}\wedge {y}={A}\setminus {x}\right)\to \left({y}\in 𝒫{A}\wedge {x}={A}\setminus {y}\right)$

### Proof

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