Theorem elpwg 4559

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-pw 4558

This theorem is used by:  elpw  4560  elpwd  4562  elpwi  4563  elpwb  4564  pwidgOLD  4577  elpwunsn  4644  elpwdifsn  4751  prsspwg  4783  elpw2g  5294  snelpwg  5410  pwvrel  5700  eldifpw  7782  elpwun  7783  elpmg  8864  fopwdom  9105  elfpw  9344  rankwflemb  9801  rankwflembOLD  9802  r1elwf  9805  r1pw  9860  ackbij1lem3  10300  lcmfval  16797  lcmf0val  16798  acsfn  17834  evls1val  22639  evls1rhm  22641  evls1sca  22642  fiinopn  23220  clsval2  23369  ssntr  23377  neipeltop  23448  nrmsep3  23674  cnrmi  23679  cmpsublem  23718  conncompss  23752  kgeni  23857  ufileu  24239  filufint  24240  elutop  24553  ustuqtop0  24560  metustss  24871  psmetutop  24887  axtgcont1  28931  elpwincl1  33164  elpwdifcl  33165  elpwiuncl  33166  dispcmp  34534  sigaclci  34807  sigainb  34812  elsigagen2  34824  sigapildsys  34838  ldgenpisyslem1  34839  rossros  34856  measvunilem  34888  measdivcstALTV  34901  ddeval1  34910  ddeval0  34911  omsfval  34969  omssubaddlem  34974  omssubadd  34975  elcarsg  34980  limsucncmpi  37308  bj-elpwg  38042  topdifinffinlem  38346  elrels2  39449  ismrcd1  43785  elpwgded  45623  snelpwrVD  45889  elpwgdedVD  45975  sspwimpcf  45978  sspwimpcfVD  45979  sspwimpALT2  45986  pwpwuni  46150  dvnprodlem2  47033  ovolsplit  47074  stoweidlem50  47136  stoweidlem57  47143  pwsal  47401  salexct  47420  fsumlesge0  47463  psmeasurelem  47556  omessle  47584  caragensplit  47586  caragenelss  47587  omecl  47589  omeunile  47591  caragenuncl  47599  caragendifcl  47600  omeunle  47602  omeiunlempt  47606  carageniuncllem2  47608  carageniuncl  47609  0ome  47615  caragencmpl  47621  ovnval2  47631  ovncvrrp  47650  ovncl  47653  ovncvr2  47697  hspmbl  47715  isvonmbl  47724  smfresal  47874  stgredgel  49131  gsumlsscl  49568  lincfsuppcl  49601  linccl  49602  lincdifsn  49612  lincellss  49614  ellcoellss  49623  lindslinindimp2lem4  49649  lindslinindsimp2lem5  49650  lindslinindsimp2  49651  lincresunit3lem2  49668  opndisj  50087