Theorem elpwg 4559

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

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

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 3920  df-pw 4558

This theorem is referenced by:  elpw  4560  elpwd  4562  elpwi  4563  elpwb  4564  pwidg  4576  elpwunsn  4643  elpwdifsn  4747  prsspwg  4781  elpw2g  5280  snelpwg  5398  pwvrel  5682  eldifpw  7723  elpwun  7724  elpmg  8792  fopwdom  9025  elfpw  9266  rankwflemb  9717  r1elwf  9720  r1pw  9769  ackbij1lem3  10143  lcmfval  16560  lcmf0val  16561  acsfn  17594  evls1val  22276  evls1rhm  22278  evls1sca  22279  fiinopn  22857  clsval2  23006  ssntr  23014  neipeltop  23085  nrmsep3  23311  cnrmi  23316  cmpsublem  23355  conncompss  23389  kgeni  23493  ufileu  23875  filufint  23876  elutop  24189  ustuqtop0  24196  metustss  24507  psmetutop  24523  axtgcont1  28552  elpwincl1  32611  elpwdifcl  32612  elpwiuncl  32613  dispcmp  34036  sigaclci  34309  sigainb  34313  elsigagen2  34325  sigapildsys  34339  ldgenpisyslem1  34340  rossros  34357  measvunilem  34389  measdivcstALTV  34402  ddeval1  34411  ddeval0  34412  omsfval  34471  omssubaddlem  34476  omssubadd  34477  elcarsg  34482  limsucncmpi  36658  bj-elpwg  37291  topdifinffinlem  37591  elrels2  38681  ismrcd1  43044  elpwgded  44909  snelpwrVD  45175  elpwgdedVD  45261  sspwimpcf  45264  sspwimpcfVD  45265  sspwimpALT2  45272  pwpwuni  45406  dvnprodlem2  46294  ovolsplit  46335  stoweidlem50  46397  stoweidlem57  46404  pwsal  46662  salexct  46681  fsumlesge0  46724  psmeasurelem  46817  omessle  46845  caragensplit  46847  caragenelss  46848  omecl  46850  omeunile  46852  caragenuncl  46860  caragendifcl  46861  omeunle  46863  omeiunlempt  46867  carageniuncllem2  46869  carageniuncl  46870  0ome  46876  caragencmpl  46882  ovnval2  46892  ovncvrrp  46911  ovncl  46914  ovncvr2  46958  hspmbl  46976  isvonmbl  46985  smfresal  47135  stgredgel  48306  gsumlsscl  48729  lincfsuppcl  48762  linccl  48763  lincdifsn  48773  lincellss  48775  ellcoellss  48784  lindslinindimp2lem4  48810  lindslinindsimp2lem5  48811  lindslinindsimp2  48812  lincresunit3lem2  48829  opndisj  49251