Theorem elpwg 4558

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

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

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 3919  df-pw 4557

This theorem is referenced by:  elpw  4559  elpwd  4561  elpwi  4562  elpwb  4563  pwidg  4575  elpwunsn  4642  elpwdifsn  4746  prsspwg  4780  elpw2g  5279  snelpwg  5392  pwvrel  5675  eldifpw  7715  elpwun  7716  elpmg  8784  fopwdom  9017  elfpw  9258  rankwflemb  9709  r1elwf  9712  r1pw  9761  ackbij1lem3  10135  lcmfval  16552  lcmf0val  16553  acsfn  17586  evls1val  22268  evls1rhm  22270  evls1sca  22271  fiinopn  22849  clsval2  22998  ssntr  23006  neipeltop  23077  nrmsep3  23303  cnrmi  23308  cmpsublem  23347  conncompss  23381  kgeni  23485  ufileu  23867  filufint  23868  elutop  24181  ustuqtop0  24188  metustss  24499  psmetutop  24515  axtgcont1  28523  elpwincl1  32582  elpwdifcl  32583  elpwiuncl  32584  dispcmp  33997  sigaclci  34270  sigainb  34274  elsigagen2  34286  sigapildsys  34300  ldgenpisyslem1  34301  rossros  34318  measvunilem  34350  measdivcstALTV  34363  ddeval1  34372  ddeval0  34373  omsfval  34432  omssubaddlem  34437  omssubadd  34438  elcarsg  34443  limsucncmpi  36620  bj-elpwg  37228  topdifinffinlem  37523  elrels2  38613  ismrcd1  42976  elpwgded  44841  snelpwrVD  45107  elpwgdedVD  45193  sspwimpcf  45196  sspwimpcfVD  45197  sspwimpALT2  45204  pwpwuni  45338  dvnprodlem2  46227  ovolsplit  46268  stoweidlem50  46330  stoweidlem57  46337  pwsal  46595  salexct  46614  fsumlesge0  46657  psmeasurelem  46750  omessle  46778  caragensplit  46780  caragenelss  46781  omecl  46783  omeunile  46785  caragenuncl  46793  caragendifcl  46794  omeunle  46796  omeiunlempt  46800  carageniuncllem2  46802  carageniuncl  46803  0ome  46809  caragencmpl  46815  ovnval2  46825  ovncvrrp  46844  ovncl  46847  ovncvr2  46891  hspmbl  46909  isvonmbl  46918  smfresal  47068  stgredgel  48239  gsumlsscl  48662  lincfsuppcl  48695  linccl  48696  lincdifsn  48706  lincellss  48708  ellcoellss  48717  lindslinindimp2lem4  48743  lindslinindsimp2lem5  48744  lindslinindsimp2  48745  lincresunit3lem2  48762  opndisj  49184