Theorem elpw2g 5247

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 4548	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5227	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4542	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 482	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 593	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 416	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 228	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  elpw2  5248  elpwi2  5249  pwnss  5250  difelpw  5252  rabelpw  5253  pw2f1olem  8621  fineqvlem  8732  elfir  8879  r1sscl  9214  tskwe  9379  dfac8alem  9455  acni2  9472  fin1ai  9715  fin2i  9717  fin23lem7  9738  fin23lem11  9739  isfin2-2  9741  fin23lem39  9772  isf34lem1  9794  isf34lem2  9795  isf34lem4  9799  isf34lem5  9800  fin1a2lem12  9833  canthnumlem  10070  tsken  10176  tskss  10180  gruss  10218  ismre  16861  mreintcl  16866  mremre  16875  submre  16876  mrcval  16881  mrccl  16882  mrcun  16893  ismri  16902  acsfiel  16925  isacs1i  16928  catcoppccl  17368  acsdrsel  17777  acsdrscl  17780  acsficl  17781  pmtrval  18579  pmtrrn  18585  istopg  21503  uniopn  21505  iscld  21635  ntrval  21644  clsval  21645  discld  21697  mretopd  21700  neival  21710  isnei  21711  lpval  21747  restdis  21786  ordtbaslem  21796  ordtuni  21798  cndis  21899  tgcmp  22009  hauscmplem  22014  comppfsc  22140  elkgen  22144  xkoopn  22197  elqtop  22305  kqffn  22333  isfbas  22437  filss  22461  snfbas  22474  elfg  22479  ufilss  22513  fixufil  22530  cfinufil  22536  ufinffr  22537  ufilen  22538  fin1aufil  22540  flimclslem  22592  hauspwpwf1  22595  supnfcls  22628  flimfnfcls  22636  ptcmplem1  22660  tsmsfbas  22736  blfvalps  22993  blfps  23016  blf  23017  bcthlem5  23931  minveclem3b  24031  sigaclcuni  31377  sigaclcu2  31379  pwsiga  31389  erdsze2lem2  32451  cvmsval  32513  cvmsss2  32521  neibastop2lem  33708  tailf  33723  pibt2  34701  fin2so  34894  sdclem1  35033  elrfirn  39312  elrfirn2  39313  istopclsd  39317  nacsfix  39329  dnnumch1  39664