Theorem elpw2g 5222

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 4508	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5201	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4502	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 483	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 594	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 417	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853  𝒫 cpw 4499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-pw 4501

This theorem is referenced by:  elpw2  5223  elpwi2OLD  5225  pwnss  5226  difelpw  5228  rabelpw  5229  pw2f1olem  8727  fineqvlem  8868  elfir  9009  r1sscl  9366  tskwe  9531  dfac8alem  9608  acni2  9625  fin1ai  9872  fin2i  9874  fin23lem7  9895  fin23lem11  9896  isfin2-2  9898  fin23lem39  9929  isf34lem1  9951  isf34lem2  9952  isf34lem4  9956  isf34lem5  9957  fin1a2lem12  9990  canthnumlem  10227  tsken  10333  tskss  10337  gruss  10375  ismre  17047  mreintcl  17052  mremre  17061  submre  17062  mrcval  17067  mrccl  17068  mrcun  17079  ismri  17088  acsfiel  17111  isacs1i  17114  catcoppccl  17577  catcoppcclOLD  17578  acsdrsel  18003  acsdrscl  18006  acsficl  18007  pmtrval  18797  pmtrrn  18803  istopg  21746  uniopn  21748  iscld  21878  ntrval  21887  clsval  21888  discld  21940  mretopd  21943  neival  21953  isnei  21954  lpval  21990  restdis  22029  ordtbaslem  22039  ordtuni  22041  cndis  22142  tgcmp  22252  hauscmplem  22257  comppfsc  22383  elkgen  22387  xkoopn  22440  elqtop  22548  kqffn  22576  isfbas  22680  filss  22704  snfbas  22717  elfg  22722  ufilss  22756  fixufil  22773  cfinufil  22779  ufinffr  22780  ufilen  22781  fin1aufil  22783  flimclslem  22835  hauspwpwf1  22838  supnfcls  22871  flimfnfcls  22879  ptcmplem1  22903  tsmsfbas  22979  blfvalps  23235  blfps  23258  blf  23259  bcthlem5  24179  minveclem3b  24279  sigaclcuni  31752  sigaclcu2  31754  pwsiga  31764  erdsze2lem2  32833  cvmsval  32895  cvmsss2  32903  neibastop2lem  34235  tailf  34250  pibt2  35274  fin2so  35450  sdclem1  35587  elrfirn  40161  elrfirn2  40162  istopclsd  40166  nacsfix  40178  dnnumch1  40513  inpw  45780