Theorem elpwg 4545

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpw  4546  elpwd  4548  elpwi  4549  elpwb  4550  pwidg  4562  elpwunsn  4629  elpwdifsn  4733  prsspwg  4767  elpw2g  5268  snelpwg  5388  pwvrel  5672  eldifpw  7713  elpwun  7714  elpmg  8781  fopwdom  9014  elfpw  9255  rankwflemb  9706  r1elwf  9709  r1pw  9758  ackbij1lem3  10132  lcmfval  16579  lcmf0val  16580  acsfn  17614  evls1val  22294  evls1rhm  22296  evls1sca  22297  fiinopn  22875  clsval2  23024  ssntr  23032  neipeltop  23103  nrmsep3  23329  cnrmi  23334  cmpsublem  23373  conncompss  23407  kgeni  23511  ufileu  23893  filufint  23894  elutop  24207  ustuqtop0  24214  metustss  24525  psmetutop  24541  axtgcont1  28555  elpwincl1  32615  elpwdifcl  32616  elpwiuncl  32617  dispcmp  34024  sigaclci  34297  sigainb  34301  elsigagen2  34313  sigapildsys  34327  ldgenpisyslem1  34328  rossros  34345  measvunilem  34377  measdivcstALTV  34390  ddeval1  34399  ddeval0  34400  omsfval  34459  omssubaddlem  34464  omssubadd  34465  elcarsg  34470  limsucncmpi  36648  bj-elpwg  37372  topdifinffinlem  37674  elrels2  38773  ismrcd1  43141  elpwgded  45006  snelpwrVD  45272  elpwgdedVD  45358  sspwimpcf  45361  sspwimpcfVD  45362  sspwimpALT2  45369  pwpwuni  45503  dvnprodlem2  46390  ovolsplit  46431  stoweidlem50  46493  stoweidlem57  46500  pwsal  46758  salexct  46777  fsumlesge0  46820  psmeasurelem  46913  omessle  46941  caragensplit  46943  caragenelss  46944  omecl  46946  omeunile  46948  caragenuncl  46956  caragendifcl  46957  omeunle  46959  omeiunlempt  46963  carageniuncllem2  46965  carageniuncl  46966  0ome  46972  caragencmpl  46978  ovnval2  46988  ovncvrrp  47007  ovncl  47010  ovncvr2  47054  hspmbl  47072  isvonmbl  47081  smfresal  47231  stgredgel  48430  gsumlsscl  48853  lincfsuppcl  48886  linccl  48887  lincdifsn  48897  lincellss  48899  ellcoellss  48908  lindslinindimp2lem4  48934  lindslinindsimp2lem5  48935  lindslinindsimp2  48936  lincresunit3lem2  48953  opndisj  49375