Theorem elpwg 4625

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  elpw  4626  elpwd  4628  elpwi  4629  elpwb  4630  pwidg  4642  elpwunsn  4707  elpwdifsn  4814  prsspwg  4848  elpw2g  5351  snelpwg  5462  pwvrel  5750  eldifpw  7803  elpwun  7804  elpmg  8901  fopwdom  9146  elfpw  9424  rankwflemb  9862  r1elwf  9865  r1pw  9914  ackbij1lem3  10290  lcmfval  16668  lcmf0val  16669  acsfn  17717  evls1val  22345  evls1rhm  22347  evls1sca  22348  fiinopn  22928  clsval2  23079  ssntr  23087  neipeltop  23158  nrmsep3  23384  cnrmi  23389  cmpsublem  23428  conncompss  23462  kgeni  23566  ufileu  23948  filufint  23949  elutop  24263  ustuqtop0  24270  metustss  24585  psmetutop  24601  axtgcont1  28494  elpwincl1  32555  elpwdifcl  32556  elpwiuncl  32557  dispcmp  33805  sigaclci  34096  sigainb  34100  elsigagen2  34112  sigapildsys  34126  ldgenpisyslem1  34127  rossros  34144  measvunilem  34176  measdivcstALTV  34189  ddeval1  34198  ddeval0  34199  omsfval  34259  omssubaddlem  34264  omssubadd  34265  elcarsg  34270  limsucncmpi  36411  bj-elpwg  37018  topdifinffinlem  37313  elrels2  38442  ismrcd1  42654  elpwgded  44535  snelpwrVD  44802  elpwgdedVD  44888  sspwimpcf  44891  sspwimpcfVD  44892  sspwimpALT2  44899  pwpwuni  44959  dvnprodlem1  45867  dvnprodlem2  45868  ovolsplit  45909  stoweidlem50  45971  stoweidlem57  45978  pwsal  46236  salexct  46255  fsumlesge0  46298  sge0f1o  46303  psmeasurelem  46391  omessle  46419  caragensplit  46421  caragenelss  46422  omecl  46424  omeunile  46426  caragenuncl  46434  caragendifcl  46435  omeunle  46437  omeiunlempt  46441  carageniuncllem2  46443  carageniuncl  46444  0ome  46450  caragencmpl  46456  ovnval2  46466  ovncvrrp  46485  ovncl  46488  ovncvr2  46532  hspmbl  46550  isvonmbl  46559  smfresal  46709  gsumlsscl  48108  lincfsuppcl  48142  linccl  48143  lincdifsn  48153  lincellss  48155  ellcoellss  48164  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lincresunit3lem2  48209  opndisj  48582