Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpwdifsn Structured version   Visualization version   GIF version

Theorem elpwdifsn 4466
 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.)
Assertion
Ref Expression
elpwdifsn ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}))

Proof of Theorem elpwdifsn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simp2 1132 . . . . . 6 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆𝑉)
21sselda 3745 . . . . 5 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥𝑉)
3 df-nel 3037 . . . . . . . . . 10 (𝐴𝑆 ↔ ¬ 𝐴𝑆)
43biimpi 206 . . . . . . . . 9 (𝐴𝑆 → ¬ 𝐴𝑆)
543ad2ant3 1130 . . . . . . . 8 ((𝑆𝑊𝑆𝑉𝐴𝑆) → ¬ 𝐴𝑆)
65anim1i 593 . . . . . . 7 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → (¬ 𝐴𝑆𝑥𝑆))
76ancomd 466 . . . . . 6 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → (𝑥𝑆 ∧ ¬ 𝐴𝑆))
8 nelne2 3030 . . . . . 6 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
97, 8syl 17 . . . . 5 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥𝐴)
10 eldifsn 4463 . . . . 5 (𝑥 ∈ (𝑉 ∖ {𝐴}) ↔ (𝑥𝑉𝑥𝐴))
112, 9, 10sylanbrc 701 . . . 4 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥 ∈ (𝑉 ∖ {𝐴}))
1211ex 449 . . 3 ((𝑆𝑊𝑆𝑉𝐴𝑆) → (𝑥𝑆𝑥 ∈ (𝑉 ∖ {𝐴})))
1312ssrdv 3751 . 2 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆 ⊆ (𝑉 ∖ {𝐴}))
14 elpwg 4311 . . 3 (𝑆𝑊 → (𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}) ↔ 𝑆 ⊆ (𝑉 ∖ {𝐴})))
15143ad2ant1 1128 . 2 ((𝑆𝑊𝑆𝑉𝐴𝑆) → (𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}) ↔ 𝑆 ⊆ (𝑉 ∖ {𝐴})))
1613, 15mpbird 247 1 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   ∈ wcel 2140   ≠ wne 2933   ∉ wnel 3036   ∖ cdif 3713   ⊆ wss 3716  𝒫 cpw 4303  {csn 4322 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-v 3343  df-dif 3719  df-in 3723  df-ss 3730  df-pw 4305  df-sn 4323 This theorem is referenced by:  uhgrspan1  26416  upgrreslem  26417  umgrreslem  26418  umgrres1lem  26423  upgrres1  26426
 Copyright terms: Public domain W3C validator