# Metamath Proof Explorer

## Theorem compsscnvlem

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

Ref Expression
Assertion compsscnvlem
`|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )`

### Proof

Step Hyp Ref Expression
1 simpr
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> y = ( A \ x ) )`
2 difss
` |-  ( A \ x ) C_ A`
3 1 2 eqsstrdi
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> y C_ A )`
4 velpw
` |-  ( y e. ~P A <-> y C_ A )`
5 3 4 sylibr
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> y e. ~P A )`
6 1 difeq2d
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( A \ y ) = ( A \ ( A \ x ) ) )`
7 elpwi
` |-  ( x e. ~P A -> x C_ A )`
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> x C_ A )`
9 dfss4
` |-  ( x C_ A <-> ( A \ ( A \ x ) ) = x )`
10 8 9 sylib
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( A \ ( A \ x ) ) = x )`
11 6 10 eqtr2d
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> x = ( A \ y ) )`
12 5 11 jca
` |-  ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )`