Theorem elpwg 4564

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2142   ⊆ wss 3904  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-pw 4563

This theorem is used by:  elpw  4565  elpwd  4567  elpwi  4568  elpwb  4569  pwidgOLD  4582  elpwunsn  4649  elpwdifsn  4756  prsspwg  4788  elpw2g  5303  snelpwg  5423  pwvrel  5710  eldifpw  7765  elpwun  7766  elpmg  8838  fopwdom  9071  elfpw  9309  rankwflemb  9763  r1elwf  9766  r1pw  9815  ackbij1lem3  10211  lcmfval  16685  lcmf0val  16686  acsfn  17721  evls1val  22491  evls1rhm  22493  evls1sca  22494  fiinopn  23069  clsval2  23218  ssntr  23226  neipeltop  23297  nrmsep3  23523  cnrmi  23528  cmpsublem  23567  conncompss  23601  kgeni  23705  ufileu  24087  filufint  24088  elutop  24401  ustuqtop0  24408  metustss  24719  psmetutop  24735  axtgcont1  28748  elpwincl1  32882  elpwdifcl  32883  elpwiuncl  32884  dispcmp  34258  sigaclci  34531  sigainb  34535  elsigagen2  34547  sigapildsys  34561  ldgenpisyslem1  34562  rossros  34579  measvunilem  34611  measdivcstALTV  34624  ddeval1  34633  ddeval0  34634  omsfval  34693  omssubaddlem  34698  omssubadd  34699  elcarsg  34704  limsucncmpi  36984  bj-elpwg  37716  topdifinffinlem  38021  elrels2  39118  ismrcd1  43457  elpwgded  45301  snelpwrVD  45567  elpwgdedVD  45653  sspwimpcf  45656  sspwimpcfVD  45657  sspwimpALT2  45664  pwpwuni  45805  dvnprodlem2  46689  ovolsplit  46730  stoweidlem50  46792  stoweidlem57  46799  pwsal  47057  salexct  47076  fsumlesge0  47119  psmeasurelem  47212  omessle  47240  caragensplit  47242  caragenelss  47243  omecl  47245  omeunile  47247  caragenuncl  47255  caragendifcl  47256  omeunle  47258  omeiunlempt  47262  carageniuncllem2  47264  carageniuncl  47265  0ome  47271  caragencmpl  47277  ovnval2  47287  ovncvrrp  47306  ovncl  47309  ovncvr2  47353  hspmbl  47371  isvonmbl  47380  smfresal  47530  stgredgel  48750  gsumlsscl  49188  lincfsuppcl  49221  linccl  49222  lincdifsn  49232  lincellss  49234  ellcoellss  49243  lindslinindimp2lem4  49269  lindslinindsimp2lem5  49270  lindslinindsimp2  49271  lincresunit3lem2  49288  opndisj  49709