Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elpwdifsn Structured version   Visualization version   GIF version

Theorem elpwdifsn 40220
 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 1054 . . . . . 6 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆𝑉)
21sselda 3472 . . . . 5 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥𝑉)
3 df-nel 2687 . . . . . . . . . 10 (𝐴𝑆 ↔ ¬ 𝐴𝑆)
43biimpi 204 . . . . . . . . 9 (𝐴𝑆 → ¬ 𝐴𝑆)
543ad2ant3 1076 . . . . . . . 8 ((𝑆𝑊𝑆𝑉𝐴𝑆) → ¬ 𝐴𝑆)
65anim1i 589 . . . . . . 7 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → (¬ 𝐴𝑆𝑥𝑆))
76ancomd 465 . . . . . 6 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → (𝑥𝑆 ∧ ¬ 𝐴𝑆))
8 nelne2 2783 . . . . . 6 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
97, 8syl 17 . . . . 5 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥𝐴)
10 eldifsn 4163 . . . . 5 (𝑥 ∈ (𝑉 ∖ {𝐴}) ↔ (𝑥𝑉𝑥𝐴))
112, 9, 10sylanbrc 694 . . . 4 (((𝑆𝑊𝑆𝑉𝐴𝑆) ∧ 𝑥𝑆) → 𝑥 ∈ (𝑉 ∖ {𝐴}))
1211ex 448 . . 3 ((𝑆𝑊𝑆𝑉𝐴𝑆) → (𝑥𝑆𝑥 ∈ (𝑉 ∖ {𝐴})))
1312ssrdv 3478 . 2 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆 ⊆ (𝑉 ∖ {𝐴}))
14 elpwg 4019 . . 3 (𝑆𝑊 → (𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}) ↔ 𝑆 ⊆ (𝑉 ∖ {𝐴})))
15143ad2ant1 1074 . 2 ((𝑆𝑊𝑆𝑉𝐴𝑆) → (𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}) ↔ 𝑆 ⊆ (𝑉 ∖ {𝐴})))
1613, 15mpbird 245 1 ((𝑆𝑊𝑆𝑉𝐴𝑆) → 𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 194   ∧ wa 382   ∧ w3a 1030   ∈ wcel 1938   ≠ wne 2684   ∉ wnel 2685   ∖ cdif 3441   ⊆ wss 3444  𝒫 cpw 4011  {csn 4028 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494 This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-v 3079  df-dif 3447  df-in 3451  df-ss 3458  df-pw 4013  df-sn 4029 This theorem is referenced by:  uhgrspan1  40632  umgrres1lem  40634  upgrres1  40637
 Copyright terms: Public domain W3C validator