Theorem elpwg 4551

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2110   ⊆ wss 3900  𝒫 cpw 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3917  df-pw 4550

This theorem is referenced by:  elpw  4552  elpwd  4554  elpwi  4555  elpwb  4556  pwidg  4568  elpwunsn  4635  elpwdifsn  4739  prsspwg  4773  elpw2g  5269  snelpwg  5382  pwvrel  5664  eldifpw  7696  elpwun  7697  elpmg  8762  fopwdom  8993  elfpw  9233  rankwflemb  9678  r1elwf  9681  r1pw  9730  ackbij1lem3  10104  lcmfval  16524  lcmf0val  16525  acsfn  17557  evls1val  22228  evls1rhm  22230  evls1sca  22231  fiinopn  22809  clsval2  22958  ssntr  22966  neipeltop  23037  nrmsep3  23263  cnrmi  23268  cmpsublem  23307  conncompss  23341  kgeni  23445  ufileu  23827  filufint  23828  elutop  24141  ustuqtop0  24148  metustss  24459  psmetutop  24475  axtgcont1  28439  elpwincl1  32495  elpwdifcl  32496  elpwiuncl  32497  dispcmp  33862  sigaclci  34135  sigainb  34139  elsigagen2  34151  sigapildsys  34165  ldgenpisyslem1  34166  rossros  34183  measvunilem  34215  measdivcstALTV  34228  ddeval1  34237  ddeval0  34238  omsfval  34297  omssubaddlem  34302  omssubadd  34303  elcarsg  34308  limsucncmpi  36458  bj-elpwg  37065  topdifinffinlem  37360  elrels2  38502  ismrcd1  42710  elpwgded  44576  snelpwrVD  44842  elpwgdedVD  44928  sspwimpcf  44931  sspwimpcfVD  44932  sspwimpALT2  44939  pwpwuni  45073  dvnprodlem2  45964  ovolsplit  46005  stoweidlem50  46067  stoweidlem57  46074  pwsal  46332  salexct  46351  fsumlesge0  46394  psmeasurelem  46487  omessle  46515  caragensplit  46517  caragenelss  46518  omecl  46520  omeunile  46522  caragenuncl  46530  caragendifcl  46531  omeunle  46533  omeiunlempt  46537  carageniuncllem2  46539  carageniuncl  46540  0ome  46546  caragencmpl  46552  ovnval2  46562  ovncvrrp  46581  ovncl  46584  ovncvr2  46628  hspmbl  46646  isvonmbl  46655  smfresal  46805  stgredgel  47967  gsumlsscl  48390  lincfsuppcl  48424  linccl  48425  lincdifsn  48435  lincellss  48437  ellcoellss  48446  lindslinindimp2lem4  48472  lindslinindsimp2lem5  48473  lindslinindsimp2  48474  lincresunit3lem2  48491  opndisj  48913