Theorem elpwg 4554

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113   ⊆ wss 3899  𝒫 cpw 4551

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3916  df-pw 4553

This theorem is referenced by:  elpw  4555  elpwd  4557  elpwi  4558  elpwb  4559  pwidg  4571  elpwunsn  4638  elpwdifsn  4742  prsspwg  4776  elpw2g  5275  snelpwg  5388  pwvrel  5671  eldifpw  7710  elpwun  7711  elpmg  8776  fopwdom  9008  elfpw  9248  rankwflemb  9696  r1elwf  9699  r1pw  9748  ackbij1lem3  10122  lcmfval  16542  lcmf0val  16543  acsfn  17575  evls1val  22245  evls1rhm  22247  evls1sca  22248  fiinopn  22826  clsval2  22975  ssntr  22983  neipeltop  23054  nrmsep3  23280  cnrmi  23285  cmpsublem  23324  conncompss  23358  kgeni  23462  ufileu  23844  filufint  23845  elutop  24158  ustuqtop0  24165  metustss  24476  psmetutop  24492  axtgcont1  28456  elpwincl1  32516  elpwdifcl  32517  elpwiuncl  32518  dispcmp  33883  sigaclci  34156  sigainb  34160  elsigagen2  34172  sigapildsys  34186  ldgenpisyslem1  34187  rossros  34204  measvunilem  34236  measdivcstALTV  34249  ddeval1  34258  ddeval0  34259  omsfval  34318  omssubaddlem  34323  omssubadd  34324  elcarsg  34329  limsucncmpi  36500  bj-elpwg  37107  topdifinffinlem  37402  elrels2  38475  ismrcd1  42805  elpwgded  44671  snelpwrVD  44937  elpwgdedVD  45023  sspwimpcf  45026  sspwimpcfVD  45027  sspwimpALT2  45034  pwpwuni  45168  dvnprodlem2  46059  ovolsplit  46100  stoweidlem50  46162  stoweidlem57  46169  pwsal  46427  salexct  46446  fsumlesge0  46489  psmeasurelem  46582  omessle  46610  caragensplit  46612  caragenelss  46613  omecl  46615  omeunile  46617  caragenuncl  46625  caragendifcl  46626  omeunle  46628  omeiunlempt  46632  carageniuncllem2  46634  carageniuncl  46635  0ome  46641  caragencmpl  46647  ovnval2  46657  ovncvrrp  46676  ovncl  46679  ovncvr2  46723  hspmbl  46741  isvonmbl  46750  smfresal  46900  stgredgel  48071  gsumlsscl  48494  lincfsuppcl  48528  linccl  48529  lincdifsn  48539  lincellss  48541  ellcoellss  48550  lindslinindimp2lem4  48576  lindslinindsimp2lem5  48577  lindslinindsimp2  48578  lincresunit3lem2  48595  opndisj  49017