Theorem elpwg 4541

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2110   ⊆ wss 3935  𝒫 cpw 4538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951  df-pw 4540

This theorem is referenced by:  elpw  4542  elpwd  4546  elpwi  4547  elpwb  4548  pwidg  4560  elpwunsn  4620  elpwdifsn  4720  prsspwg  4755  elpw2g  5246  pwvrel  5601  eldifpw  7489  elpwun  7490  elpmg  8421  fopwdom  8624  elfpw  8825  rankwflemb  9221  r1elwf  9224  r1pw  9273  ackbij1lem3  9643  lcmfval  15964  lcmf0val  15965  acsfn  16929  evls1val  20482  evls1rhm  20484  evls1sca  20485  fiinopn  21508  clsval2  21657  ssntr  21665  neipeltop  21736  nrmsep3  21962  cnrmi  21967  cmpsublem  22006  conncompss  22040  kgeni  22144  ufileu  22526  filufint  22527  elutop  22841  ustuqtop0  22848  metustss  23160  psmetutop  23176  axtgcont1  26253  elpwincl1  30285  elpwdifcl  30286  elpwiuncl  30287  dispcmp  31123  sigaclci  31391  sigainb  31395  elsigagen2  31407  sigapildsys  31421  ldgenpisyslem1  31422  rossros  31439  measvunilem  31471  measdivcstALTV  31484  ddeval1  31493  ddeval0  31494  omsfval  31552  omssubaddlem  31557  omssubadd  31558  elcarsg  31563  limsucncmpi  33793  bj-elpwg  34344  topdifinffinlem  34627  elrels2  35725  ismrcd1  39293  elpwgded  40896  snelpwrVD  41163  elpwgdedVD  41249  sspwimpcf  41252  sspwimpcfVD  41253  sspwimpALT2  41260  pwpwuni  41317  dvnprodlem1  42229  dvnprodlem2  42230  ovolsplit  42272  stoweidlem50  42334  stoweidlem57  42341  pwsal  42599  saliuncl  42606  salexct  42616  fsumlesge0  42658  sge0f1o  42663  psmeasurelem  42751  omessle  42779  caragensplit  42781  caragenelss  42782  omecl  42784  omeunile  42786  caragenuncl  42794  caragendifcl  42795  omeunle  42797  omeiunlempt  42801  carageniuncllem2  42803  carageniuncl  42804  0ome  42810  caragencmpl  42816  ovnval2  42826  ovncvrrp  42845  ovncl  42848  ovncvr2  42892  hspmbl  42910  isvonmbl  42919  smfresal  43062  gsumlsscl  44430  lincfsuppcl  44467  linccl  44468  lincdifsn  44478  lincellss  44480  ellcoellss  44489  lindslinindimp2lem4  44515  lindslinindsimp2lem5  44516  lindslinindsimp2  44517  lincresunit3lem2  44534