Theorem elpwg 4533

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  elpw  4534  elpwd  4538  elpwi  4539  elpwb  4540  pwidg  4552  elpwunsn  4616  elpwdifsn  4719  prsspwg  4753  elpw2g  5263  pwvrel  5628  eldifpw  7596  elpwun  7597  elpmg  8589  fopwdom  8820  elfpw  9051  rankwflemb  9482  r1elwf  9485  r1pw  9534  ackbij1lem3  9909  lcmfval  16254  lcmf0val  16255  acsfn  17285  evls1val  21396  evls1rhm  21398  evls1sca  21399  fiinopn  21958  clsval2  22109  ssntr  22117  neipeltop  22188  nrmsep3  22414  cnrmi  22419  cmpsublem  22458  conncompss  22492  kgeni  22596  ufileu  22978  filufint  22979  elutop  23293  ustuqtop0  23300  metustss  23613  psmetutop  23629  axtgcont1  26733  elpwincl1  30775  elpwdifcl  30776  elpwiuncl  30777  dispcmp  31711  sigaclci  32000  sigainb  32004  elsigagen2  32016  sigapildsys  32030  ldgenpisyslem1  32031  rossros  32048  measvunilem  32080  measdivcstALTV  32093  ddeval1  32102  ddeval0  32103  omsfval  32161  omssubaddlem  32166  omssubadd  32167  elcarsg  32172  limsucncmpi  34561  bj-elpwg  35152  topdifinffinlem  35445  elrels2  36531  ismrcd1  40436  elpwgded  42073  snelpwrVD  42340  elpwgdedVD  42426  sspwimpcf  42429  sspwimpcfVD  42430  sspwimpALT2  42437  pwpwuni  42494  dvnprodlem1  43377  dvnprodlem2  43378  ovolsplit  43419  stoweidlem50  43481  stoweidlem57  43488  pwsal  43746  saliuncl  43753  salexct  43763  fsumlesge0  43805  sge0f1o  43810  psmeasurelem  43898  omessle  43926  caragensplit  43928  caragenelss  43929  omecl  43931  omeunile  43933  caragenuncl  43941  caragendifcl  43942  omeunle  43944  omeiunlempt  43948  carageniuncllem2  43950  carageniuncl  43951  0ome  43957  caragencmpl  43963  ovnval2  43973  ovncvrrp  43992  ovncl  43995  ovncvr2  44039  hspmbl  44057  isvonmbl  44066  smfresal  44209  gsumlsscl  45607  lincfsuppcl  45642  linccl  45643  lincdifsn  45653  lincellss  45655  ellcoellss  45664  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  lincresunit3lem2  45709  opndisj  46084