Theorem elpwg 4559

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 3955	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4558	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3633	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145   ⊆ wss 3898  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3915  df-pw 4558

This theorem is used by:  elpw  4560  elpwd  4562  elpwi  4563  elpwb  4564  pwidgOLD  4577  elpwunsn  4644  elpwdifsn  4751  prsspwg  4783  elpw2g  5294  snelpwg  5410  pwvrel  5697  eldifpw  7765  elpwun  7766  elpmg  8841  fopwdom  9082  elfpw  9321  rankwflemb  9775  r1elwf  9778  r1pw  9832  ackbij1lem3  10271  lcmfval  16759  lcmf0val  16760  acsfn  17795  evls1val  22600  evls1rhm  22602  evls1sca  22603  fiinopn  23181  clsval2  23330  ssntr  23338  neipeltop  23409  nrmsep3  23635  cnrmi  23640  cmpsublem  23679  conncompss  23713  kgeni  23818  ufileu  24200  filufint  24201  elutop  24514  ustuqtop0  24521  metustss  24832  psmetutop  24848  axtgcont1  28864  elpwincl1  33055  elpwdifcl  33056  elpwiuncl  33057  dispcmp  34425  sigaclci  34698  sigainb  34703  elsigagen2  34715  sigapildsys  34729  ldgenpisyslem1  34730  rossros  34747  measvunilem  34779  measdivcstALTV  34792  ddeval1  34801  ddeval0  34802  omsfval  34861  omssubaddlem  34866  omssubadd  34867  elcarsg  34872  limsucncmpi  37155  bj-elpwg  37887  topdifinffinlem  38190  elrels2  39293  ismrcd1  43647  elpwgded  45491  snelpwrVD  45757  elpwgdedVD  45843  sspwimpcf  45846  sspwimpcfVD  45847  sspwimpALT2  45854  pwpwuni  45995  dvnprodlem2  46879  ovolsplit  46920  stoweidlem50  46982  stoweidlem57  46989  pwsal  47247  salexct  47266  fsumlesge0  47309  psmeasurelem  47402  omessle  47430  caragensplit  47432  caragenelss  47433  omecl  47435  omeunile  47437  caragenuncl  47445  caragendifcl  47446  omeunle  47448  omeiunlempt  47452  carageniuncllem2  47454  carageniuncl  47455  0ome  47461  caragencmpl  47467  ovnval2  47477  ovncvrrp  47496  ovncl  47499  ovncvr2  47543  hspmbl  47561  isvonmbl  47570  smfresal  47720  stgredgel  48977  gsumlsscl  49414  lincfsuppcl  49447  linccl  49448  lincdifsn  49458  lincellss  49460  ellcoellss  49469  lindslinindimp2lem4  49495  lindslinindsimp2lem5  49496  lindslinindsimp2  49497  lincresunit3lem2  49514  opndisj  49933