Theorem elpwg 4607

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2105   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-pw 4606

This theorem is referenced by:  elpw  4608  elpwd  4610  elpwi  4611  elpwb  4612  pwidg  4624  elpwunsn  4688  elpwdifsn  4793  prsspwg  4827  elpw2g  5338  snelpwg  5452  pwvrel  5738  eldifpw  7786  elpwun  7787  elpmg  8881  fopwdom  9118  elfpw  9391  rankwflemb  9830  r1elwf  9833  r1pw  9882  ackbij1lem3  10258  lcmfval  16654  lcmf0val  16655  acsfn  17703  evls1val  22339  evls1rhm  22341  evls1sca  22342  fiinopn  22922  clsval2  23073  ssntr  23081  neipeltop  23152  nrmsep3  23378  cnrmi  23383  cmpsublem  23422  conncompss  23456  kgeni  23560  ufileu  23942  filufint  23943  elutop  24257  ustuqtop0  24264  metustss  24579  psmetutop  24595  axtgcont1  28490  elpwincl1  32552  elpwdifcl  32553  elpwiuncl  32554  dispcmp  33819  sigaclci  34112  sigainb  34116  elsigagen2  34128  sigapildsys  34142  ldgenpisyslem1  34143  rossros  34160  measvunilem  34192  measdivcstALTV  34205  ddeval1  34214  ddeval0  34215  omsfval  34275  omssubaddlem  34280  omssubadd  34281  elcarsg  34286  limsucncmpi  36427  bj-elpwg  37034  topdifinffinlem  37329  elrels2  38467  ismrcd1  42685  elpwgded  44561  snelpwrVD  44828  elpwgdedVD  44914  sspwimpcf  44917  sspwimpcfVD  44918  sspwimpALT2  44925  pwpwuni  44996  dvnprodlem2  45902  ovolsplit  45943  stoweidlem50  46005  stoweidlem57  46012  pwsal  46270  salexct  46289  fsumlesge0  46332  psmeasurelem  46425  omessle  46453  caragensplit  46455  caragenelss  46456  omecl  46458  omeunile  46460  caragenuncl  46468  caragendifcl  46469  omeunle  46471  omeiunlempt  46475  carageniuncllem2  46477  carageniuncl  46478  0ome  46484  caragencmpl  46490  ovnval2  46500  ovncvrrp  46519  ovncl  46522  ovncvr2  46566  hspmbl  46584  isvonmbl  46593  smfresal  46743  stgredgel  47859  gsumlsscl  48224  lincfsuppcl  48258  linccl  48259  lincdifsn  48269  lincellss  48271  ellcoellss  48280  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lincresunit3lem2  48325  opndisj  48698