Theorem elpwg 4564

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2141   ⊆ wss 3904  𝒫 cpw 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-pw 4563

This theorem is referenced by:  elpw  4565  elpwd  4567  elpwi  4568  elpwb  4569  pwidgOLD  4582  elpwunsn  4649  elpwdifsn  4756  prsspwg  4788  elpw2g  5303  snelpwg  5424  pwvrel  5711  eldifpw  7766  elpwun  7767  elpmg  8839  fopwdom  9072  elfpw  9310  rankwflemb  9764  r1elwf  9767  r1pw  9816  ackbij1lem3  10203  lcmfval  16678  lcmf0val  16679  acsfn  17714  evls1val  22459  evls1rhm  22461  evls1sca  22462  fiinopn  23037  clsval2  23186  ssntr  23194  neipeltop  23265  nrmsep3  23491  cnrmi  23496  cmpsublem  23535  conncompss  23569  kgeni  23673  ufileu  24055  filufint  24056  elutop  24369  ustuqtop0  24376  metustss  24687  psmetutop  24703  axtgcont1  28713  elpwincl1  32837  elpwdifcl  32838  elpwiuncl  32839  dispcmp  34215  sigaclci  34488  sigainb  34492  elsigagen2  34504  sigapildsys  34518  ldgenpisyslem1  34519  rossros  34536  measvunilem  34568  measdivcstALTV  34581  ddeval1  34590  ddeval0  34591  omsfval  34650  omssubaddlem  34655  omssubadd  34656  elcarsg  34661  limsucncmpi  36922  bj-elpwg  37654  topdifinffinlem  37959  elrels2  39058  ismrcd1  43399  elpwgded  45243  snelpwrVD  45509  elpwgdedVD  45595  sspwimpcf  45598  sspwimpcfVD  45599  sspwimpALT2  45606  pwpwuni  45747  dvnprodlem2  46631  ovolsplit  46672  stoweidlem50  46734  stoweidlem57  46741  pwsal  46999  salexct  47018  fsumlesge0  47061  psmeasurelem  47154  omessle  47182  caragensplit  47184  caragenelss  47185  omecl  47187  omeunile  47189  caragenuncl  47197  caragendifcl  47198  omeunle  47200  omeiunlempt  47204  carageniuncllem2  47206  carageniuncl  47207  0ome  47213  caragencmpl  47219  ovnval2  47229  ovncvrrp  47248  ovncl  47251  ovncvr2  47295  hspmbl  47313  isvonmbl  47322  smfresal  47472  stgredgel  48689  gsumlsscl  49127  lincfsuppcl  49160  linccl  49161  lincdifsn  49171  lincellss  49173  ellcoellss  49182  lindslinindimp2lem4  49208  lindslinindsimp2lem5  49209  lindslinindsimp2  49210  lincresunit3lem2  49227  opndisj  49648