Theorem elpwg 4561

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5294. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.)

Assertion

Ref	Expression
elpwg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Proof of Theorem elpwg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 3964	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4560	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3642	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2145   ⊆ wss 3907  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-pw 4560

This theorem is referenced by:  elpw  4562  elpwd  4564  elpwi  4565  elpwb  4566  pwidgOLD  4579  elpwunsn  4646  elpwdifsn  4752  prsspwg  4784  elpw2g  5294  snelpwg  5415  pwvrel  5702  eldifpw  7755  elpwun  7756  elpmg  8828  fopwdom  9061  elfpw  9299  rankwflemb  9753  r1elwf  9756  r1pw  9805  ackbij1lem3  10192  lcmfval  16669  lcmf0val  16670  acsfn  17705  evls1val  22441  evls1rhm  22443  evls1sca  22444  fiinopn  23019  clsval2  23168  ssntr  23176  neipeltop  23247  nrmsep3  23473  cnrmi  23478  cmpsublem  23517  conncompss  23551  kgeni  23655  ufileu  24037  filufint  24038  elutop  24351  ustuqtop0  24358  metustss  24669  psmetutop  24685  axtgcont1  28695  elpwincl1  32781  elpwdifcl  32782  elpwiuncl  32783  dispcmp  34166  sigaclci  34439  sigainb  34443  elsigagen2  34455  sigapildsys  34469  ldgenpisyslem1  34470  rossros  34487  measvunilem  34519  measdivcstALTV  34532  ddeval1  34541  ddeval0  34542  omsfval  34601  omssubaddlem  34606  omssubadd  34607  elcarsg  34612  limsucncmpi  36818  bj-elpwg  37549  topdifinffinlem  37853  elrels2  38952  ismrcd1  43291  elpwgded  45138  snelpwrVD  45404  elpwgdedVD  45490  sspwimpcf  45493  sspwimpcfVD  45494  sspwimpALT2  45501  pwpwuni  45635  dvnprodlem2  46519  ovolsplit  46560  stoweidlem50  46622  stoweidlem57  46629  pwsal  46887  salexct  46906  fsumlesge0  46949  psmeasurelem  47042  omessle  47070  caragensplit  47072  caragenelss  47073  omecl  47075  omeunile  47077  caragenuncl  47085  caragendifcl  47086  omeunle  47088  omeiunlempt  47092  carageniuncllem2  47094  carageniuncl  47095  0ome  47101  caragencmpl  47107  ovnval2  47117  ovncvrrp  47136  ovncl  47139  ovncvr2  47183  hspmbl  47201  isvonmbl  47210  smfresal  47360  stgredgel  48577  gsumlsscl  49011  lincfsuppcl  49044  linccl  49045  lincdifsn  49055  lincellss  49057  ellcoellss  49066  lindslinindimp2lem4  49092  lindslinindsimp2lem5  49093  lindslinindsimp2  49094  lincresunit3lem2  49111  opndisj  49532