Theorem elpw2g 5275

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

Step	Hyp	Ref	Expression
1		elpwi 4560	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5265	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4556	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 226	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922  df-pw 4555

This theorem is referenced by:  elpw2  5276  rabelpw  5278  difelpw  5296  pw2f1olem  9005  fineqvlem  9167  elfir  9324  r1sscl  9700  tskwe  9865  dfac8alem  9942  acni2  9959  fin1ai  10206  fin2i  10208  fin23lem7  10229  fin23lem11  10230  isfin2-2  10232  fin23lem39  10263  isf34lem1  10285  isf34lem2  10286  isf34lem4  10290  isf34lem5  10291  fin1a2lem12  10324  canthnumlem  10561  tsken  10667  tskss  10671  gruss  10709  ismre  17510  mreintcl  17515  mremre  17524  submre  17525  mrcval  17534  mrccl  17535  mrcun  17546  ismri  17555  acsfiel  17578  isacs1i  17581  catcoppccl  18042  acsdrsel  18467  acsdrscl  18470  acsficl  18471  pmtrval  19348  pmtrrn  19354  istopg  22798  uniopn  22800  iscld  22930  ntrval  22939  clsval  22940  discld  22992  mretopd  22995  neival  23005  isnei  23006  lpval  23042  restdis  23081  ordtbaslem  23091  ordtuni  23093  cndis  23194  tgcmp  23304  hauscmplem  23309  comppfsc  23435  elkgen  23439  xkoopn  23492  elqtop  23600  kqffn  23628  isfbas  23732  filss  23756  snfbas  23769  elfg  23774  ufilss  23808  fixufil  23825  cfinufil  23831  ufinffr  23832  ufilen  23833  fin1aufil  23835  flimclslem  23887  hauspwpwf1  23890  supnfcls  23923  flimfnfcls  23931  ptcmplem1  23955  tsmsfbas  24031  blfvalps  24287  blfps  24310  blf  24311  bcthlem5  25244  minveclem3b  25344  sigaclcuni  34084  sigaclcu2  34086  pwsiga  34096  erdsze2lem2  35176  cvmsval  35238  cvmsss2  35246  neibastop2lem  36333  tailf  36348  pibt2  37390  fin2so  37586  sdclem1  37722  elrfirn  42668  elrfirn2  42669  istopclsd  42673  nacsfix  42685  dnnumch1  43017  inpw  48797