Theorem elpwg 4500

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5211. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.)

Assertion

Ref	Expression
elpwg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Proof of Theorem elpwg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 3940	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵))
2		sseq1 3940	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
3		df-pw 4499	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
4	1, 2, 3	elab2gw 3613	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111   ⊆ wss 3881  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  elpw  4501  elpwd  4505  elpwi  4506  elpwb  4507  pwidg  4519  elpwunsn  4581  elpwdifsn  4682  prsspwg  4716  elpw2g  5211  pwvrel  5566  eldifpw  7470  elpwun  7471  elpmg  8405  fopwdom  8608  elfpw  8810  rankwflemb  9206  r1elwf  9209  r1pw  9258  ackbij1lem3  9633  lcmfval  15955  lcmf0val  15956  acsfn  16922  evls1val  20944  evls1rhm  20946  evls1sca  20947  fiinopn  21506  clsval2  21655  ssntr  21663  neipeltop  21734  nrmsep3  21960  cnrmi  21965  cmpsublem  22004  conncompss  22038  kgeni  22142  ufileu  22524  filufint  22525  elutop  22839  ustuqtop0  22846  metustss  23158  psmetutop  23174  axtgcont1  26262  elpwincl1  30298  elpwdifcl  30299  elpwiuncl  30300  dispcmp  31212  sigaclci  31501  sigainb  31505  elsigagen2  31517  sigapildsys  31531  ldgenpisyslem1  31532  rossros  31549  measvunilem  31581  measdivcstALTV  31594  ddeval1  31603  ddeval0  31604  omsfval  31662  omssubaddlem  31667  omssubadd  31668  elcarsg  31673  limsucncmpi  33906  bj-elpwg  34469  topdifinffinlem  34764  elrels2  35886  ismrcd1  39639  elpwgded  41270  snelpwrVD  41537  elpwgdedVD  41623  sspwimpcf  41626  sspwimpcfVD  41627  sspwimpALT2  41634  pwpwuni  41691  dvnprodlem1  42588  dvnprodlem2  42589  ovolsplit  42630  stoweidlem50  42692  stoweidlem57  42699  pwsal  42957  saliuncl  42964  salexct  42974  fsumlesge0  43016  sge0f1o  43021  psmeasurelem  43109  omessle  43137  caragensplit  43139  caragenelss  43140  omecl  43142  omeunile  43144  caragenuncl  43152  caragendifcl  43153  omeunle  43155  omeiunlempt  43159  carageniuncllem2  43161  carageniuncl  43162  0ome  43168  caragencmpl  43174  ovnval2  43184  ovncvrrp  43203  ovncl  43206  ovncvr2  43250  hspmbl  43268  isvonmbl  43277  smfresal  43420  gsumlsscl  44785  lincfsuppcl  44822  linccl  44823  lincdifsn  44833  lincellss  44835  ellcoellss  44844  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  lincresunit3lem2  44889