Theorem elpwg 4556

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 3963	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4555	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3638	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  elpw  4557  elpwd  4559  elpwi  4560  elpwb  4561  pwidg  4573  elpwunsn  4638  elpwdifsn  4743  prsspwg  4777  elpw2g  5275  snelpwg  5389  pwvrel  5673  eldifpw  7708  elpwun  7709  elpmg  8777  fopwdom  9009  elfpw  9263  rankwflemb  9708  r1elwf  9711  r1pw  9760  ackbij1lem3  10134  lcmfval  16550  lcmf0val  16551  acsfn  17583  evls1val  22223  evls1rhm  22225  evls1sca  22226  fiinopn  22804  clsval2  22953  ssntr  22961  neipeltop  23032  nrmsep3  23258  cnrmi  23263  cmpsublem  23302  conncompss  23336  kgeni  23440  ufileu  23822  filufint  23823  elutop  24137  ustuqtop0  24144  metustss  24455  psmetutop  24471  axtgcont1  28431  elpwincl1  32487  elpwdifcl  32488  elpwiuncl  32489  dispcmp  33825  sigaclci  34098  sigainb  34102  elsigagen2  34114  sigapildsys  34128  ldgenpisyslem1  34129  rossros  34146  measvunilem  34178  measdivcstALTV  34191  ddeval1  34200  ddeval0  34201  omsfval  34261  omssubaddlem  34266  omssubadd  34267  elcarsg  34272  limsucncmpi  36418  bj-elpwg  37025  topdifinffinlem  37320  elrels2  38462  ismrcd1  42671  elpwgded  44538  snelpwrVD  44804  elpwgdedVD  44890  sspwimpcf  44893  sspwimpcfVD  44894  sspwimpALT2  44901  pwpwuni  45035  dvnprodlem2  45929  ovolsplit  45970  stoweidlem50  46032  stoweidlem57  46039  pwsal  46297  salexct  46316  fsumlesge0  46359  psmeasurelem  46452  omessle  46480  caragensplit  46482  caragenelss  46483  omecl  46485  omeunile  46487  caragenuncl  46495  caragendifcl  46496  omeunle  46498  omeiunlempt  46502  carageniuncllem2  46504  carageniuncl  46505  0ome  46511  caragencmpl  46517  ovnval2  46527  ovncvrrp  46546  ovncl  46549  ovncvr2  46593  hspmbl  46611  isvonmbl  46620  smfresal  46770  stgredgel  47940  gsumlsscl  48352  lincfsuppcl  48386  linccl  48387  lincdifsn  48397  lincellss  48399  ellcoellss  48408  lindslinindimp2lem4  48434  lindslinindsimp2lem5  48435  lindslinindsimp2  48436  lincresunit3lem2  48453  opndisj  48875