Theorem elpwg 4544

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114   ⊆ wss 3938  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  elpw  4545  elpwd  4549  elpwi  4550  elpwb  4551  pwidg  4563  elpwunsn  4623  elpwdifsn  4723  prsspwg  4758  elpw2g  5249  pwvrel  5604  eldifpw  7492  elpwun  7493  elpmg  8424  fopwdom  8627  elfpw  8828  rankwflemb  9224  r1elwf  9227  r1pw  9276  ackbij1lem3  9646  lcmfval  15967  lcmf0val  15968  acsfn  16932  evls1val  20485  evls1rhm  20487  evls1sca  20488  fiinopn  21511  clsval2  21660  ssntr  21668  neipeltop  21739  nrmsep3  21965  cnrmi  21970  cmpsublem  22009  conncompss  22043  kgeni  22147  ufileu  22529  filufint  22530  elutop  22844  ustuqtop0  22851  metustss  23163  psmetutop  23179  axtgcont1  26256  elpwincl1  30288  elpwdifcl  30289  elpwiuncl  30290  dispcmp  31125  sigaclci  31393  sigainb  31397  elsigagen2  31409  sigapildsys  31423  ldgenpisyslem1  31424  rossros  31441  measvunilem  31473  measdivcstALTV  31486  ddeval1  31495  ddeval0  31496  omsfval  31554  omssubaddlem  31559  omssubadd  31560  elcarsg  31565  limsucncmpi  33795  bj-elpwg  34347  topdifinffinlem  34630  elrels2  35728  ismrcd1  39302  elpwgded  40905  snelpwrVD  41172  elpwgdedVD  41258  sspwimpcf  41261  sspwimpcfVD  41262  sspwimpALT2  41269  pwpwuni  41326  dvnprodlem1  42238  dvnprodlem2  42239  ovolsplit  42280  stoweidlem50  42342  stoweidlem57  42349  pwsal  42607  saliuncl  42614  salexct  42624  fsumlesge0  42666  sge0f1o  42671  psmeasurelem  42759  omessle  42787  caragensplit  42789  caragenelss  42790  omecl  42792  omeunile  42794  caragenuncl  42802  caragendifcl  42803  omeunle  42805  omeiunlempt  42809  carageniuncllem2  42811  carageniuncl  42812  0ome  42818  caragencmpl  42824  ovnval2  42834  ovncvrrp  42853  ovncl  42856  ovncvr2  42900  hspmbl  42918  isvonmbl  42927  smfresal  43070  gsumlsscl  44438  lincfsuppcl  44475  linccl  44476  lincdifsn  44486  lincellss  44488  ellcoellss  44497  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  lincresunit3lem2  44542