Theorem elpwg 4539

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  elpw  4540  elpwd  4542  elpwi  4543  elpwb  4544  pwidg  4556  elpwunsn  4623  elpwdifsn  4729  prsspwg  4761  elpw2g  5268  snelpwg  5389  pwvrel  5675  eldifpw  7718  elpwun  7719  elpmg  8787  fopwdom  9020  elfpw  9261  rankwflemb  9715  r1elwf  9718  r1pw  9767  ackbij1lem3  10141  lcmfval  16588  lcmf0val  16589  acsfn  17623  evls1val  22313  evls1rhm  22315  evls1sca  22316  fiinopn  22891  clsval2  23040  ssntr  23048  neipeltop  23119  nrmsep3  23345  cnrmi  23350  cmpsublem  23389  conncompss  23423  kgeni  23527  ufileu  23909  filufint  23910  elutop  24223  ustuqtop0  24230  metustss  24541  psmetutop  24557  axtgcont1  28561  elpwincl1  32620  elpwdifcl  32621  elpwiuncl  32622  dispcmp  34050  sigaclci  34323  sigainb  34327  elsigagen2  34339  sigapildsys  34353  ldgenpisyslem1  34354  rossros  34371  measvunilem  34403  measdivcstALTV  34416  ddeval1  34425  ddeval0  34426  omsfval  34485  omssubaddlem  34490  omssubadd  34491  elcarsg  34496  limsucncmpi  36674  bj-elpwg  37406  topdifinffinlem  37710  elrels2  38809  ismrcd1  43148  elpwgded  45009  snelpwrVD  45275  elpwgdedVD  45361  sspwimpcf  45364  sspwimpcfVD  45365  sspwimpALT2  45372  pwpwuni  45506  dvnprodlem2  46391  ovolsplit  46432  stoweidlem50  46494  stoweidlem57  46501  pwsal  46759  salexct  46778  fsumlesge0  46821  psmeasurelem  46914  omessle  46942  caragensplit  46944  caragenelss  46945  omecl  46947  omeunile  46949  caragenuncl  46957  caragendifcl  46958  omeunle  46960  omeiunlempt  46964  carageniuncllem2  46966  carageniuncl  46967  0ome  46973  caragencmpl  46979  ovnval2  46989  ovncvrrp  47008  ovncl  47011  ovncvr2  47055  hspmbl  47073  isvonmbl  47082  smfresal  47232  stgredgel  48449  gsumlsscl  48872  lincfsuppcl  48905  linccl  48906  lincdifsn  48916  lincellss  48918  ellcoellss  48927  lindslinindimp2lem4  48953  lindslinindsimp2lem5  48954  lindslinindsimp2  48955  lincresunit3lem2  48972  opndisj  49394