Theorem elpwg 4545

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpw  4546  elpwd  4548  elpwi  4549  elpwb  4550  pwidg  4562  elpwunsn  4629  elpwdifsn  4735  prsspwg  4767  elpw2g  5275  snelpwg  5396  pwvrel  5681  eldifpw  7722  elpwun  7723  elpmg  8790  fopwdom  9023  elfpw  9264  rankwflemb  9717  r1elwf  9720  r1pw  9769  ackbij1lem3  10143  lcmfval  16590  lcmf0val  16591  acsfn  17625  evls1val  22285  evls1rhm  22287  evls1sca  22288  fiinopn  22866  clsval2  23015  ssntr  23023  neipeltop  23094  nrmsep3  23320  cnrmi  23325  cmpsublem  23364  conncompss  23398  kgeni  23502  ufileu  23884  filufint  23885  elutop  24198  ustuqtop0  24205  metustss  24516  psmetutop  24532  axtgcont1  28536  elpwincl1  32595  elpwdifcl  32596  elpwiuncl  32597  dispcmp  34003  sigaclci  34276  sigainb  34280  elsigagen2  34292  sigapildsys  34306  ldgenpisyslem1  34307  rossros  34324  measvunilem  34356  measdivcstALTV  34369  ddeval1  34378  ddeval0  34379  omsfval  34438  omssubaddlem  34443  omssubadd  34444  elcarsg  34449  limsucncmpi  36627  bj-elpwg  37359  topdifinffinlem  37663  elrels2  38762  ismrcd1  43130  elpwgded  44991  snelpwrVD  45257  elpwgdedVD  45343  sspwimpcf  45346  sspwimpcfVD  45347  sspwimpALT2  45354  pwpwuni  45488  dvnprodlem2  46375  ovolsplit  46416  stoweidlem50  46478  stoweidlem57  46485  pwsal  46743  salexct  46762  fsumlesge0  46805  psmeasurelem  46898  omessle  46926  caragensplit  46928  caragenelss  46929  omecl  46931  omeunile  46933  caragenuncl  46941  caragendifcl  46942  omeunle  46944  omeiunlempt  46948  carageniuncllem2  46950  carageniuncl  46951  0ome  46957  caragencmpl  46963  ovnval2  46973  ovncvrrp  46992  ovncl  46995  ovncvr2  47039  hspmbl  47057  isvonmbl  47066  smfresal  47216  stgredgel  48427  gsumlsscl  48850  lincfsuppcl  48883  linccl  48884  lincdifsn  48894  lincellss  48896  ellcoellss  48905  lindslinindimp2lem4  48931  lindslinindsimp2lem5  48932  lindslinindsimp2  48933  lincresunit3lem2  48950  opndisj  49372