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

Metamath Proof Explorer

Theorem elpwdifsn

Description: A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020)

Ref Expression
Assertion elpwdifsn 
|- ( ( S e. W /\ S C_ V /\ A e/ S ) -> S e. ~P ( V \ { A } ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> S C_ V )
2 1 sselda 
 |-  ( ( ( S e. W /\ S C_ V /\ A e/ S ) /\ x e. S ) -> x e. V )
3 df-nel 
 |-  ( A e/ S <-> -. A e. S )
4 3 biimpi 
 |-  ( A e/ S -> -. A e. S )
5 4 3ad2ant3 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> -. A e. S )
6 5 anim1ci 
 |-  ( ( ( S e. W /\ S C_ V /\ A e/ S ) /\ x e. S ) -> ( x e. S /\ -. A e. S ) )
7 nelne2 
 |-  ( ( x e. S /\ -. A e. S ) -> x =/= A )
8 6 7 syl 
 |-  ( ( ( S e. W /\ S C_ V /\ A e/ S ) /\ x e. S ) -> x =/= A )
9 eldifsn 
 |-  ( x e. ( V \ { A } ) <-> ( x e. V /\ x =/= A ) )
10 2 8 9 sylanbrc 
 |-  ( ( ( S e. W /\ S C_ V /\ A e/ S ) /\ x e. S ) -> x e. ( V \ { A } ) )
11 10 ex 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> ( x e. S -> x e. ( V \ { A } ) ) )
12 11 ssrdv 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> S C_ ( V \ { A } ) )
13 elpwg 
 |-  ( S e. W -> ( S e. ~P ( V \ { A } ) <-> S C_ ( V \ { A } ) ) )
14 13 3ad2ant1 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> ( S e. ~P ( V \ { A } ) <-> S C_ ( V \ { A } ) ) )
15 12 14 mpbird 
 |-  ( ( S e. W /\ S C_ V /\ A e/ S ) -> S e. ~P ( V \ { A } ) )