Theorem elpwg 4552

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2136   ⊆ wss 3899  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ss 3916  df-pw 4551

This theorem is referenced by:  elpw  4553  elpwd  4555  elpwi  4556  elpwb  4557  pwidgOLD  4570  elpwunsn  4637  elpwdifsn  4743  prsspwg  4775  elpw2g  5283  snelpwg  5404  pwvrel  5690  eldifpw  7740  elpwun  7741  elpmg  8813  fopwdom  9046  elfpw  9287  rankwflemb  9741  r1elwf  9744  r1pw  9793  ackbij1lem3  10167  lcmfval  16631  lcmf0val  16632  acsfn  17667  evls1val  22356  evls1rhm  22358  evls1sca  22359  fiinopn  22934  clsval2  23083  ssntr  23091  neipeltop  23162  nrmsep3  23388  cnrmi  23393  cmpsublem  23432  conncompss  23466  kgeni  23570  ufileu  23952  filufint  23953  elutop  24266  ustuqtop0  24273  metustss  24584  psmetutop  24600  axtgcont1  28607  elpwincl1  32666  elpwdifcl  32667  elpwiuncl  32668  dispcmp  34110  sigaclci  34383  sigainb  34387  elsigagen2  34399  sigapildsys  34413  ldgenpisyslem1  34414  rossros  34431  measvunilem  34463  measdivcstALTV  34476  ddeval1  34485  ddeval0  34486  omsfval  34545  omssubaddlem  34550  omssubadd  34551  elcarsg  34556  limsucncmpi  36753  bj-elpwg  37485  topdifinffinlem  37789  elrels2  38888  ismrcd1  43227  elpwgded  45088  snelpwrVD  45354  elpwgdedVD  45440  sspwimpcf  45443  sspwimpcfVD  45444  sspwimpALT2  45451  pwpwuni  45585  dvnprodlem2  46469  ovolsplit  46510  stoweidlem50  46572  stoweidlem57  46579  pwsal  46837  salexct  46856  fsumlesge0  46899  psmeasurelem  46992  omessle  47020  caragensplit  47022  caragenelss  47023  omecl  47025  omeunile  47027  caragenuncl  47035  caragendifcl  47036  omeunle  47038  omeiunlempt  47042  carageniuncllem2  47044  carageniuncl  47045  0ome  47051  caragencmpl  47057  ovnval2  47067  ovncvrrp  47086  ovncl  47089  ovncvr2  47133  hspmbl  47151  isvonmbl  47160  smfresal  47310  stgredgel  48527  gsumlsscl  48950  lincfsuppcl  48983  linccl  48984  lincdifsn  48994  lincellss  48996  ellcoellss  49005  lindslinindimp2lem4  49031  lindslinindsimp2lem5  49032  lindslinindsimp2  49033  lincresunit3lem2  49050  opndisj  49472