Theorem elpw2g 5249

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 4550	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5229	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4544	. . . . 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 3496   ⊆ wss 3938  𝒫 cpw 4541

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 2795  ax-sep 5205

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  elpw2  5250  elpwi2  5251  pwnss  5252  difelpw  5254  rabelpw  5255  pw2f1olem  8623  fineqvlem  8734  elfir  8881  r1sscl  9216  tskwe  9381  dfac8alem  9457  acni2  9474  fin1ai  9717  fin2i  9719  fin23lem7  9740  fin23lem11  9741  isfin2-2  9743  fin23lem39  9774  isf34lem1  9796  isf34lem2  9797  isf34lem4  9801  isf34lem5  9802  fin1a2lem12  9835  canthnumlem  10072  tsken  10178  tskss  10182  gruss  10220  ismre  16863  mreintcl  16868  mremre  16877  submre  16878  mrcval  16883  mrccl  16884  mrcun  16895  ismri  16904  acsfiel  16927  isacs1i  16930  catcoppccl  17370  acsdrsel  17779  acsdrscl  17782  acsficl  17783  pmtrval  18581  pmtrrn  18587  istopg  21505  uniopn  21507  iscld  21637  ntrval  21646  clsval  21647  discld  21699  mretopd  21702  neival  21712  isnei  21713  lpval  21749  restdis  21788  ordtbaslem  21798  ordtuni  21800  cndis  21901  tgcmp  22011  hauscmplem  22016  comppfsc  22142  elkgen  22146  xkoopn  22199  elqtop  22307  kqffn  22335  isfbas  22439  filss  22463  snfbas  22476  elfg  22481  ufilss  22515  fixufil  22532  cfinufil  22538  ufinffr  22539  ufilen  22540  fin1aufil  22542  flimclslem  22594  hauspwpwf1  22597  supnfcls  22630  flimfnfcls  22638  ptcmplem1  22662  tsmsfbas  22738  blfvalps  22995  blfps  23018  blf  23019  bcthlem5  23933  minveclem3b  24033  sigaclcuni  31379  sigaclcu2  31381  pwsiga  31391  erdsze2lem2  32453  cvmsval  32515  cvmsss2  32523  neibastop2lem  33710  tailf  33725  pibt2  34700  fin2so  34881  sdclem1  35020  elrfirn  39299  elrfirn2  39300  istopclsd  39304  nacsfix  39316  dnnumch1  39651