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 } ) )