ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elpw2g GIF version

Theorem elpw2g 4168
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
Assertion
Ref Expression
elpw2g (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Proof of Theorem elpw2g
StepHypRef Expression
1 elpwi 3596 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 4154 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 3595 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 299 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 282 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 116 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 143 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wcel 2158  Vcvv 2749  wss 3141  𝒫 cpw 3587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-sep 4133
This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-in 3147  df-ss 3154  df-pw 3589
This theorem is referenced by:  elpw2  4169  pwnss  4171  ifelpwung  4493  elfir  6986  issubm  12885  issubg  13065  issubrng  13419  issubrg  13441  islssm  13546  islssmg  13547  lspval  13579  lspcl  13580  sraval  13626  istopg  13795  uniopn  13797  iscld  13899  ntrval  13906  clsval  13907  discld  13932  neival  13939  isnei  13940  restdis  13980  cnpfval  13991  cndis  14037  blfvalps  14181  blfps  14205  blf  14206  reldvg  14444
  Copyright terms: Public domain W3C validator