Theorem elpwg 4563

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-pw 4562

This theorem is used by:  elpw  4564  elpwd  4566  elpwi  4567  elpwb  4568  pwidgOLD  4581  elpwunsn  4648  elpwdifsn  4755  prsspwg  4787  elpw2g  5302  snelpwg  5422  pwvrel  5709  eldifpw  7770  elpwun  7771  elpmg  8845  fopwdom  9086  elfpw  9324  rankwflemb  9778  r1elwf  9781  r1pw  9830  ackbij1lem3  10226  lcmfval  16715  lcmf0val  16716  acsfn  17751  evls1val  22549  evls1rhm  22551  evls1sca  22552  fiinopn  23130  clsval2  23279  ssntr  23287  neipeltop  23358  nrmsep3  23584  cnrmi  23589  cmpsublem  23628  conncompss  23662  kgeni  23767  ufileu  24149  filufint  24150  elutop  24463  ustuqtop0  24470  metustss  24781  psmetutop  24797  axtgcont1  28810  elpwincl1  33001  elpwdifcl  33002  elpwiuncl  33003  dispcmp  34371  sigaclci  34644  sigainb  34649  elsigagen2  34661  sigapildsys  34675  ldgenpisyslem1  34676  rossros  34693  measvunilem  34725  measdivcstALTV  34738  ddeval1  34747  ddeval0  34748  omsfval  34807  omssubaddlem  34812  omssubadd  34813  elcarsg  34818  limsucncmpi  37066  bj-elpwg  37798  topdifinffinlem  38103  elrels2  39191  ismrcd1  43545  elpwgded  45389  snelpwrVD  45655  elpwgdedVD  45741  sspwimpcf  45744  sspwimpcfVD  45745  sspwimpALT2  45752  pwpwuni  45893  dvnprodlem2  46777  ovolsplit  46818  stoweidlem50  46880  stoweidlem57  46887  pwsal  47145  salexct  47164  fsumlesge0  47207  psmeasurelem  47300  omessle  47328  caragensplit  47330  caragenelss  47331  omecl  47333  omeunile  47335  caragenuncl  47343  caragendifcl  47344  omeunle  47346  omeiunlempt  47350  carageniuncllem2  47352  carageniuncl  47353  0ome  47359  caragencmpl  47365  ovnval2  47375  ovncvrrp  47394  ovncl  47397  ovncvr2  47441  hspmbl  47459  isvonmbl  47468  smfresal  47618  stgredgel  48875  gsumlsscl  49312  lincfsuppcl  49345  linccl  49346  lincdifsn  49356  lincellss  49358  ellcoellss  49367  lindslinindimp2lem4  49393  lindslinindsimp2lem5  49394  lindslinindsimp2  49395  lincresunit3lem2  49412  opndisj  49831