Theorem elpwg 4566

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-pw 4565

This theorem is referenced by:  elpw  4567  elpwd  4569  elpwi  4570  elpwb  4571  pwidg  4583  elpwunsn  4648  elpwdifsn  4753  prsspwg  4787  elpw2g  5288  snelpwg  5402  pwvrel  5688  eldifpw  7744  elpwun  7745  elpmg  8816  fopwdom  9049  elfpw  9305  rankwflemb  9746  r1elwf  9749  r1pw  9798  ackbij1lem3  10174  lcmfval  16591  lcmf0val  16592  acsfn  17620  evls1val  22207  evls1rhm  22209  evls1sca  22210  fiinopn  22788  clsval2  22937  ssntr  22945  neipeltop  23016  nrmsep3  23242  cnrmi  23247  cmpsublem  23286  conncompss  23320  kgeni  23424  ufileu  23806  filufint  23807  elutop  24121  ustuqtop0  24128  metustss  24439  psmetutop  24455  axtgcont1  28395  elpwincl1  32454  elpwdifcl  32455  elpwiuncl  32456  dispcmp  33849  sigaclci  34122  sigainb  34126  elsigagen2  34138  sigapildsys  34152  ldgenpisyslem1  34153  rossros  34170  measvunilem  34202  measdivcstALTV  34215  ddeval1  34224  ddeval0  34225  omsfval  34285  omssubaddlem  34290  omssubadd  34291  elcarsg  34296  limsucncmpi  36433  bj-elpwg  37040  topdifinffinlem  37335  elrels2  38477  ismrcd1  42686  elpwgded  44554  snelpwrVD  44820  elpwgdedVD  44906  sspwimpcf  44909  sspwimpcfVD  44910  sspwimpALT2  44917  pwpwuni  45051  dvnprodlem2  45945  ovolsplit  45986  stoweidlem50  46048  stoweidlem57  46055  pwsal  46313  salexct  46332  fsumlesge0  46375  psmeasurelem  46468  omessle  46496  caragensplit  46498  caragenelss  46499  omecl  46501  omeunile  46503  caragenuncl  46511  caragendifcl  46512  omeunle  46514  omeiunlempt  46518  carageniuncllem2  46520  carageniuncl  46521  0ome  46527  caragencmpl  46533  ovnval2  46543  ovncvrrp  46562  ovncl  46565  ovncvr2  46609  hspmbl  46627  isvonmbl  46636  smfresal  46786  stgredgel  47956  gsumlsscl  48368  lincfsuppcl  48402  linccl  48403  lincdifsn  48413  lincellss  48415  ellcoellss  48424  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lincresunit3lem2  48469  opndisj  48891