Theorem elpwg 4536

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5268. (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 3946	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4535	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3611	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  elpw  4537  elpwd  4541  elpwi  4542  elpwb  4543  pwidg  4555  elpwunsn  4619  elpwdifsn  4722  prsspwg  4756  elpw2g  5268  pwvrel  5637  eldifpw  7618  elpwun  7619  elpmg  8631  fopwdom  8867  elfpw  9121  rankwflemb  9551  r1elwf  9554  r1pw  9603  ackbij1lem3  9978  lcmfval  16326  lcmf0val  16327  acsfn  17368  evls1val  21486  evls1rhm  21488  evls1sca  21489  fiinopn  22050  clsval2  22201  ssntr  22209  neipeltop  22280  nrmsep3  22506  cnrmi  22511  cmpsublem  22550  conncompss  22584  kgeni  22688  ufileu  23070  filufint  23071  elutop  23385  ustuqtop0  23392  metustss  23707  psmetutop  23723  axtgcont1  26829  elpwincl1  30874  elpwdifcl  30875  elpwiuncl  30876  dispcmp  31809  sigaclci  32100  sigainb  32104  elsigagen2  32116  sigapildsys  32130  ldgenpisyslem1  32131  rossros  32148  measvunilem  32180  measdivcstALTV  32193  ddeval1  32202  ddeval0  32203  omsfval  32261  omssubaddlem  32266  omssubadd  32267  elcarsg  32272  limsucncmpi  34634  bj-elpwg  35225  topdifinffinlem  35518  elrels2  36604  ismrcd1  40520  elpwgded  42184  snelpwrVD  42451  elpwgdedVD  42537  sspwimpcf  42540  sspwimpcfVD  42541  sspwimpALT2  42548  pwpwuni  42605  dvnprodlem1  43487  dvnprodlem2  43488  ovolsplit  43529  stoweidlem50  43591  stoweidlem57  43598  pwsal  43856  saliuncl  43863  salexct  43873  fsumlesge0  43915  sge0f1o  43920  psmeasurelem  44008  omessle  44036  caragensplit  44038  caragenelss  44039  omecl  44041  omeunile  44043  caragenuncl  44051  caragendifcl  44052  omeunle  44054  omeiunlempt  44058  carageniuncllem2  44060  carageniuncl  44061  0ome  44067  caragencmpl  44073  ovnval2  44083  ovncvrrp  44102  ovncl  44105  ovncvr2  44149  hspmbl  44167  isvonmbl  44176  smfresal  44322  gsumlsscl  45719  lincfsuppcl  45754  linccl  45755  lincdifsn  45765  lincellss  45767  ellcoellss  45776  lindslinindimp2lem4  45802  lindslinindsimp2lem5  45803  lindslinindsimp2  45804  lincresunit3lem2  45821  opndisj  46196