Theorem elpwg 4563

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-pw 4562

This theorem is used by:  elpw  4564  elpwd  4566  elpwi  4567  elpwb  4568  pwidgOLD  4582  elpwunsn  4645  elpwdifsn  4752  prsspwg  4782  elpw2g  5299  snelpwg  5415  pwvrel  5705  eldifpw  7806  elpwun  7807  elpmg  8891  fopwdom  9132  elfpw  9371  rankwflemb  9827  rankwflembOLD  9828  r1elwf  9831  r1pw  9886  ackbij1lem3  10326  lcmfval  16825  lcmf0val  16826  acsfn  17862  evls1val  22668  evls1rhm  22670  evls1sca  22671  fiinopn  23249  clsval2  23398  ssntr  23406  neipeltop  23477  nrmsep3  23703  cnrmi  23708  cmpsublem  23747  conncompss  23781  kgeni  23886  ufileu  24268  filufint  24269  elutop  24582  ustuqtop0  24589  metustss  24900  psmetutop  24916  axtgcont1  28960  elpwincl1  33193  elpwdifcl  33194  elpwiuncl  33195  dispcmp  34561  sigaclci  34834  sigainb  34839  elsigagen2  34851  sigapildsys  34865  ldgenpisyslem1  34866  rossros  34883  measvunilem  34915  measdivcstALTV  34928  ddeval1  34937  ddeval0  34938  omsfval  34996  omssubaddlem  35001  omssubadd  35002  elcarsg  35007  limsucncmpi  37411  bj-elpwg  38158  topdifinffinlem  38462  elrels2  39565  ismrcd1  43902  elpwgded  45738  snelpwrVD  46004  elpwgdedVD  46090  sspwimpcf  46093  sspwimpcfVD  46094  sspwimpALT2  46101  pwpwuni  46279  dvnprodlem2  47162  ovolsplit  47203  stoweidlem50  47265  stoweidlem57  47272  pwsal  47530  salexct  47549  fsumlesge0  47592  psmeasurelem  47685  omessle  47713  caragensplit  47715  caragenelss  47716  omecl  47718  omeunile  47720  caragenuncl  47728  caragendifcl  47729  omeunle  47731  omeiunlempt  47735  carageniuncllem2  47737  carageniuncl  47738  0ome  47744  caragencmpl  47750  ovnval2  47760  ovncvrrp  47779  ovncl  47782  ovncvr2  47826  hspmbl  47844  isvonmbl  47853  smfresal  48003  stgredgel  49260  gsumlsscl  49697  lincfsuppcl  49730  linccl  49731  lincdifsn  49741  lincellss  49743  ellcoellss  49752  lindslinindimp2lem4  49778  lindslinindsimp2lem5  49779  lindslinindsimp2  49780  lincresunit3lem2  49797  opndisj  50222