Theorem elpwg 4116

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4754. (Contributed by NM, 6-Aug-2000.)

Assertion

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

Proof of Theorem elpwg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2676	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝒫 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵))
2		sseq1 3589	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
3		selpw 4115	. 2 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
4	1, 2, 3	vtoclbg 3240	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  elpwi  4117  pwidg  4121  elpwunsn  4171  prsspwg  4295  sselpwd  4734  elpw2g  4754  pwel  4847  f1opw2  6786  eldifpw  6868  elpwun  6869  elpmg  7759  fopwdom  7953  elfpw  8151  f1opwfi  8153  rankwflemb  8539  r1elwf  8542  r1pw  8591  ackbij1lem3  8927  ackbij1lem6  8930  ackbij1lem11  8935  lcmfval  15172  lcmf0val  15173  mreexexlemd  16127  acsfn  16143  evls1val  19506  evls1rhm  19508  evls1sca  19509  fiinopn  20531  clsval2  20664  ssntr  20672  neipeltop  20743  nrmsep3  20969  cnrmi  20974  cmpcov  21002  cmpsublem  21012  concompss  21046  kgeni  21150  tgqtop  21325  filss  21467  ufileu  21533  filufint  21534  elutop  21847  ustuqtop0  21854  metustss  22166  psmetutop  22182  axtgcont1  25167  elpwincl1  28741  elpwdifcl  28742  elpwiuncl  28743  elpwunicl  28754  crefi  29242  dispcmp  29254  pcmplfin  29255  indval  29403  isrnsigaOLD  29502  sigaclci  29522  sigainb  29526  elsigagen2  29538  sigapildsys  29552  ldgenpisyslem1  29553  rossros  29570  measvunilem  29602  measdivcstOLD  29614  ddeval1  29624  ddeval0  29625  omsfval  29683  omssubaddlem  29688  omssubadd  29689  elcarsg  29694  limsucncmpi  31614  bj-elpw3  32237  topdifinffinlem  32371  ismrcd1  36279  elpwgded  37801  snelpwrVD  38088  elpwgdedVD  38175  sspwimpcf  38178  sspwimpcfVD  38179  sspwimpALT2  38186  pwpwuni  38250  elpwd  38264  wessf1ornlem  38366  dvnprodlem1  38836  dvnprodlem2  38837  ovolsplit  38881  stoweidlem50  38943  stoweidlem57  38950  pwsal  39211  saliuncl  39218  salexct  39228  fsumlesge0  39270  sge0f1o  39275  meadjuni  39350  psmeasurelem  39363  omessle  39388  caragensplit  39390  caragenelss  39391  omecl  39393  omeunile  39395  caragenuncl  39403  caragendifcl  39404  omeunle  39406  omeiunlempt  39410  carageniuncllem2  39412  carageniuncl  39413  0ome  39419  caragencmpl  39425  ovnval2  39435  ovncvrrp  39454  ovncl  39457  ovncvr2  39501  hspmbl  39519  isvonmbl  39528  smfresal  39673  elpwdifsn  40312  gsumlsscl  41958  lincfsuppcl  41996  linccl  41997  lincdifsn  42007  lincellss  42009  ellcoellss  42018  lindslinindsimp1  42040  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lincresunit3lem2  42063  lincresunit3  42064