Theorem elpw2g 4976

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 4312	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 4956	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4310	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 505	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 488	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 450	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 216	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715  𝒫 cpw 4302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-pw 4304

This theorem is referenced by:  elpw2  4977  elpwi2  4978  pwnss  4979  pw2f1olem  8229  fineqvlem  8339  elfir  8486  marypha1  8505  r1sscl  8821  tskwe  8966  dfac8alem  9042  acni2  9059  fin1ai  9307  fin2i  9309  fin23lem7  9330  fin23lem11  9331  isfin2-2  9333  fin23lem39  9364  isf34lem1  9386  isf34lem2  9387  isf34lem4  9391  isf34lem5  9392  fin1a2lem12  9425  canthnumlem  9662  canthp1lem2  9667  tsken  9768  tskss  9772  gruss  9810  ramub1lem1  15932  ismre  16452  mreintcl  16457  mremre  16466  submre  16467  mrcval  16472  mrccl  16473  mrcun  16484  ismri  16493  mreexexlem4d  16509  acsfiel  16516  isacs1i  16519  catcoppccl  16959  acsdrsel  17368  acsdrscl  17371  acsficl  17372  pmtrval  18071  pmtrrn  18077  opsrval  19676  istopg  20902  uniopn  20904  iscld  21033  ntrval  21042  clsval  21043  discld  21095  mretopd  21098  neival  21108  isnei  21109  lpval  21145  restdis  21184  ordtbaslem  21194  ordtuni  21196  cncls  21280  cndis  21297  tgcmp  21406  hauscmplem  21411  comppfsc  21537  elkgen  21541  xkoopn  21594  elqtop  21702  kqffn  21730  isfbas  21834  filss  21858  snfbas  21871  elfg  21876  fbasrn  21889  ufilss  21910  fixufil  21927  cfinufil  21933  ufinffr  21934  ufilen  21935  fin1aufil  21937  rnelfmlem  21957  flimclslem  21989  hauspwpwf1  21992  supnfcls  22025  flimfnfcls  22033  ptcmplem1  22057  tsmsfbas  22132  blfvalps  22389  blfps  22412  blf  22413  bcthlem5  23325  minveclem3b  23399  sigaclcuni  30490  sigaclcu2  30492  pwsiga  30502  erdsze2lem2  31493  cvmsval  31555  cvmsss2  31563  neibastop2lem  32661  tailf  32676  bj-ismoored  33368  fin2so  33709  sdclem1  33852  elrfirn  37760  elrfirn2  37761  istopclsd  37765  nacsfix  37777  dnnumch1  38116