# 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 ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to {S}\in 𝒫\left({V}\setminus \left\{{A}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 simp2 ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to {S}\subseteq {V}$
2 1 sselda ${⊢}\left(\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\wedge {x}\in {S}\right)\to {x}\in {V}$
3 df-nel ${⊢}{A}\notin {S}↔¬{A}\in {S}$
4 3 biimpi ${⊢}{A}\notin {S}\to ¬{A}\in {S}$
5 4 3ad2ant3 ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to ¬{A}\in {S}$
6 5 anim1ci ${⊢}\left(\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\wedge {x}\in {S}\right)\to \left({x}\in {S}\wedge ¬{A}\in {S}\right)$
7 nelne2 ${⊢}\left({x}\in {S}\wedge ¬{A}\in {S}\right)\to {x}\ne {A}$
8 6 7 syl ${⊢}\left(\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\wedge {x}\in {S}\right)\to {x}\ne {A}$
9 eldifsn ${⊢}{x}\in \left({V}\setminus \left\{{A}\right\}\right)↔\left({x}\in {V}\wedge {x}\ne {A}\right)$
10 2 8 9 sylanbrc ${⊢}\left(\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\wedge {x}\in {S}\right)\to {x}\in \left({V}\setminus \left\{{A}\right\}\right)$
11 10 ex ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to \left({x}\in {S}\to {x}\in \left({V}\setminus \left\{{A}\right\}\right)\right)$
12 11 ssrdv ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to {S}\subseteq {V}\setminus \left\{{A}\right\}$
13 elpwg ${⊢}{S}\in {W}\to \left({S}\in 𝒫\left({V}\setminus \left\{{A}\right\}\right)↔{S}\subseteq {V}\setminus \left\{{A}\right\}\right)$
14 13 3ad2ant1 ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to \left({S}\in 𝒫\left({V}\setminus \left\{{A}\right\}\right)↔{S}\subseteq {V}\setminus \left\{{A}\right\}\right)$
15 12 14 mpbird ${⊢}\left({S}\in {W}\wedge {S}\subseteq {V}\wedge {A}\notin {S}\right)\to {S}\in 𝒫\left({V}\setminus \left\{{A}\right\}\right)$