Theorem elpwg 4578

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 3984	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4577	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3659	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-pw 4577

This theorem is referenced by:  elpw  4579  elpwd  4581  elpwi  4582  elpwb  4583  pwidg  4595  elpwunsn  4660  elpwdifsn  4765  prsspwg  4799  elpw2g  5303  snelpwg  5417  pwvrel  5704  eldifpw  7762  elpwun  7763  elpmg  8857  fopwdom  9094  elfpw  9366  rankwflemb  9807  r1elwf  9810  r1pw  9859  ackbij1lem3  10235  lcmfval  16640  lcmf0val  16641  acsfn  17671  evls1val  22258  evls1rhm  22260  evls1sca  22261  fiinopn  22839  clsval2  22988  ssntr  22996  neipeltop  23067  nrmsep3  23293  cnrmi  23298  cmpsublem  23337  conncompss  23371  kgeni  23475  ufileu  23857  filufint  23858  elutop  24172  ustuqtop0  24179  metustss  24490  psmetutop  24506  axtgcont1  28447  elpwincl1  32506  elpwdifcl  32507  elpwiuncl  32508  dispcmp  33890  sigaclci  34163  sigainb  34167  elsigagen2  34179  sigapildsys  34193  ldgenpisyslem1  34194  rossros  34211  measvunilem  34243  measdivcstALTV  34256  ddeval1  34265  ddeval0  34266  omsfval  34326  omssubaddlem  34331  omssubadd  34332  elcarsg  34337  limsucncmpi  36463  bj-elpwg  37070  topdifinffinlem  37365  elrels2  38504  ismrcd1  42721  elpwgded  44589  snelpwrVD  44855  elpwgdedVD  44941  sspwimpcf  44944  sspwimpcfVD  44945  sspwimpALT2  44952  pwpwuni  45081  dvnprodlem2  45976  ovolsplit  46017  stoweidlem50  46079  stoweidlem57  46086  pwsal  46344  salexct  46363  fsumlesge0  46406  psmeasurelem  46499  omessle  46527  caragensplit  46529  caragenelss  46530  omecl  46532  omeunile  46534  caragenuncl  46542  caragendifcl  46543  omeunle  46545  omeiunlempt  46549  carageniuncllem2  46551  carageniuncl  46552  0ome  46558  caragencmpl  46564  ovnval2  46574  ovncvrrp  46593  ovncl  46596  ovncvr2  46640  hspmbl  46658  isvonmbl  46667  smfresal  46817  stgredgel  47969  gsumlsscl  48355  lincfsuppcl  48389  linccl  48390  lincdifsn  48400  lincellss  48402  ellcoellss  48411  lindslinindimp2lem4  48437  lindslinindsimp2lem5  48438  lindslinindsimp2  48439  lincresunit3lem2  48456  opndisj  48877