Theorem elpwg 4542

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2110   ⊆ wss 3892  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-pw 4541

This theorem is referenced by:  elpw  4543  elpwd  4547  elpwi  4548  elpwb  4549  pwidg  4561  elpwunsn  4625  elpwdifsn  4728  prsspwg  4762  elpw2g  5272  pwvrel  5638  eldifpw  7613  elpwun  7614  elpmg  8623  fopwdom  8858  elfpw  9109  rankwflemb  9562  r1elwf  9565  r1pw  9614  ackbij1lem3  9989  lcmfval  16337  lcmf0val  16338  acsfn  17379  evls1val  21497  evls1rhm  21499  evls1sca  21500  fiinopn  22061  clsval2  22212  ssntr  22220  neipeltop  22291  nrmsep3  22517  cnrmi  22522  cmpsublem  22561  conncompss  22595  kgeni  22699  ufileu  23081  filufint  23082  elutop  23396  ustuqtop0  23403  metustss  23718  psmetutop  23734  axtgcont1  26840  elpwincl1  30883  elpwdifcl  30884  elpwiuncl  30885  dispcmp  31818  sigaclci  32109  sigainb  32113  elsigagen2  32125  sigapildsys  32139  ldgenpisyslem1  32140  rossros  32157  measvunilem  32189  measdivcstALTV  32202  ddeval1  32211  ddeval0  32212  omsfval  32270  omssubaddlem  32275  omssubadd  32276  elcarsg  32281  limsucncmpi  34643  bj-elpwg  35234  topdifinffinlem  35527  elrels2  36613  ismrcd1  40529  elpwgded  42166  snelpwrVD  42433  elpwgdedVD  42519  sspwimpcf  42522  sspwimpcfVD  42523  sspwimpALT2  42530  pwpwuni  42587  dvnprodlem1  43469  dvnprodlem2  43470  ovolsplit  43511  stoweidlem50  43573  stoweidlem57  43580  pwsal  43838  saliuncl  43845  salexct  43855  fsumlesge0  43897  sge0f1o  43902  psmeasurelem  43990  omessle  44018  caragensplit  44020  caragenelss  44021  omecl  44023  omeunile  44025  caragenuncl  44033  caragendifcl  44034  omeunle  44036  omeiunlempt  44040  carageniuncllem2  44042  carageniuncl  44043  0ome  44049  caragencmpl  44055  ovnval2  44065  ovncvrrp  44084  ovncl  44087  ovncvr2  44131  hspmbl  44149  isvonmbl  44158  smfresal  44301  gsumlsscl  45698  lincfsuppcl  45733  linccl  45734  lincdifsn  45744  lincellss  45746  ellcoellss  45755  lindslinindimp2lem4  45781  lindslinindsimp2lem5  45782  lindslinindsimp2  45783  lincresunit3lem2  45800  opndisj  46175