Theorem elpwg 4569

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  elpw  4570  elpwd  4572  elpwi  4573  elpwb  4574  pwidg  4586  elpwunsn  4651  elpwdifsn  4756  prsspwg  4790  elpw2g  5291  snelpwg  5405  pwvrel  5691  eldifpw  7747  elpwun  7748  elpmg  8819  fopwdom  9054  elfpw  9312  rankwflemb  9753  r1elwf  9756  r1pw  9805  ackbij1lem3  10181  lcmfval  16598  lcmf0val  16599  acsfn  17627  evls1val  22214  evls1rhm  22216  evls1sca  22217  fiinopn  22795  clsval2  22944  ssntr  22952  neipeltop  23023  nrmsep3  23249  cnrmi  23254  cmpsublem  23293  conncompss  23327  kgeni  23431  ufileu  23813  filufint  23814  elutop  24128  ustuqtop0  24135  metustss  24446  psmetutop  24462  axtgcont1  28402  elpwincl1  32461  elpwdifcl  32462  elpwiuncl  32463  dispcmp  33856  sigaclci  34129  sigainb  34133  elsigagen2  34145  sigapildsys  34159  ldgenpisyslem1  34160  rossros  34177  measvunilem  34209  measdivcstALTV  34222  ddeval1  34231  ddeval0  34232  omsfval  34292  omssubaddlem  34297  omssubadd  34298  elcarsg  34303  limsucncmpi  36440  bj-elpwg  37047  topdifinffinlem  37342  elrels2  38484  ismrcd1  42693  elpwgded  44561  snelpwrVD  44827  elpwgdedVD  44913  sspwimpcf  44916  sspwimpcfVD  44917  sspwimpALT2  44924  pwpwuni  45058  dvnprodlem2  45952  ovolsplit  45993  stoweidlem50  46055  stoweidlem57  46062  pwsal  46320  salexct  46339  fsumlesge0  46382  psmeasurelem  46475  omessle  46503  caragensplit  46505  caragenelss  46506  omecl  46508  omeunile  46510  caragenuncl  46518  caragendifcl  46519  omeunle  46521  omeiunlempt  46525  carageniuncllem2  46527  carageniuncl  46528  0ome  46534  caragencmpl  46540  ovnval2  46550  ovncvrrp  46569  ovncl  46572  ovncvr2  46616  hspmbl  46634  isvonmbl  46643  smfresal  46793  stgredgel  47960  gsumlsscl  48372  lincfsuppcl  48406  linccl  48407  lincdifsn  48417  lincellss  48419  ellcoellss  48428  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lincresunit3lem2  48473  opndisj  48895