Theorem elpwg 4599

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-pw 4598

This theorem is referenced by:  elpw  4600  elpwd  4602  elpwi  4603  elpwb  4604  pwidg  4616  elpwunsn  4680  elpwdifsn  4785  prsspwg  4819  elpw2g  5337  snelpwg  5435  pwvrel  5718  eldifpw  7738  elpwun  7739  elpmg  8820  fopwdom  9063  elfpw  9337  rankwflemb  9770  r1elwf  9773  r1pw  9822  ackbij1lem3  10199  lcmfval  16540  lcmf0val  16541  acsfn  17585  evls1val  21768  evls1rhm  21770  evls1sca  21771  fiinopn  22332  clsval2  22483  ssntr  22491  neipeltop  22562  nrmsep3  22788  cnrmi  22793  cmpsublem  22832  conncompss  22866  kgeni  22970  ufileu  23352  filufint  23353  elutop  23667  ustuqtop0  23674  metustss  23989  psmetutop  24005  axtgcont1  27584  elpwincl1  31628  elpwdifcl  31629  elpwiuncl  31630  dispcmp  32670  sigaclci  32961  sigainb  32965  elsigagen2  32977  sigapildsys  32991  ldgenpisyslem1  32992  rossros  33009  measvunilem  33041  measdivcstALTV  33054  ddeval1  33063  ddeval0  33064  omsfval  33124  omssubaddlem  33129  omssubadd  33130  elcarsg  33135  limsucncmpi  35134  bj-elpwg  35737  topdifinffinlem  36032  elrels2  37161  ismrcd1  41207  elpwgded  43096  snelpwrVD  43363  elpwgdedVD  43449  sspwimpcf  43452  sspwimpcfVD  43453  sspwimpALT2  43460  pwpwuni  43515  dvnprodlem1  44435  dvnprodlem2  44436  ovolsplit  44477  stoweidlem50  44539  stoweidlem57  44546  pwsal  44804  salexct  44823  fsumlesge0  44866  sge0f1o  44871  psmeasurelem  44959  omessle  44987  caragensplit  44989  caragenelss  44990  omecl  44992  omeunile  44994  caragenuncl  45002  caragendifcl  45003  omeunle  45005  omeiunlempt  45009  carageniuncllem2  45011  carageniuncl  45012  0ome  45018  caragencmpl  45024  ovnval2  45034  ovncvrrp  45053  ovncl  45056  ovncvr2  45100  hspmbl  45118  isvonmbl  45127  smfresal  45277  gsumlsscl  46707  lincfsuppcl  46742  linccl  46743  lincdifsn  46753  lincellss  46755  ellcoellss  46764  lindslinindimp2lem4  46790  lindslinindsimp2lem5  46791  lindslinindsimp2  46792  lincresunit3lem2  46809  opndisj  47183