Theorem selpw 4115

Description: Setvar variable membership in a power class (common case). See elpw 4114. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
selpw	⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem selpw

Step	Hyp	Ref	Expression
1		vex 3176	. 2 ⊢ 𝑥 ∈ V
2	1	elpw 4114	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 195   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  elpwg  4116  pwss  4123  snsspw  4315  pwpr  4368  pwtp  4369  pwv  4371  sspwuni  4547  iinpw  4550  iunpwss  4551  pwuni  4825  ssextss  4849  pwin  4942  pwunss  4943  sorpsscmpl  6846  iunpw  6870  ordpwsuc  6907  fabexg  7015  abexssex  7041  qsss  7695  mapval2  7773  pmsspw  7778  uniixp  7817  fineqvlem  8059  fival  8201  hartogslem1  8330  tskwe  8659  cfval2  8965  cflim3  8967  cflim2  8968  cfslb  8971  compsscnvlem  9075  fin1a2lem13  9117  axdc3lem  9155  fpwwe2lem1  9332  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe  9347  canthwe  9352  axgroth5  9525  axgroth6  9529  wuncn  9870  ishashinf  13104  vdwmc  15520  ramub2  15556  ram0  15564  restsspw  15915  ismred  16085  mremre  16087  mreacs  16142  acsfn  16143  submacs  17188  subgacs  17452  nsgacs  17453  sylow2alem2  17856  sylow2a  17857  sylow3lem3  17867  sylow3lem6  17870  dprdres  18250  subgdmdprd  18256  pgpfac1lem5  18301  subrgmre  18627  subsubrg2  18630  lssintcl  18785  lssmre  18787  lssacs  18788  cssmre  19856  istopon  20540  isbasis2g  20563  tgval2  20571  unitg  20582  distop  20610  cldss2  20644  ntreq0  20691  discld  20703  toponmre  20707  neisspw  20721  restdis  20792  cnntr  20889  isnrm2  20972  cmpcovf  21004  fincmp  21006  cmpsublem  21012  cmpsub  21013  cmpcld  21015  cmpfi  21021  is1stc2  21055  2ndcdisj  21069  llyi  21087  nllyi  21088  nlly2i  21089  llynlly  21090  subislly  21094  restnlly  21095  llyrest  21098  llyidm  21101  nllyidm  21102  islocfin  21130  ptuni2  21189  prdstopn  21241  qtoptop2  21312  qtopuni  21315  tgqtop  21325  isfbas2  21449  isfild  21472  elfg  21485  cfinfil  21507  csdfil  21508  supfil  21509  isufil2  21522  filssufilg  21525  uffix  21535  ufildr  21545  fin1aufil  21546  alexsubb  21660  alexsubALTlem1  21661  alexsubALT  21665  ptcmplem5  21670  cldsubg  21724  ustfn  21815  ustfilxp  21826  ustn0  21834  dscopn  22188  voliunlem2  23126  vitali  23188  shex  27453  dfch2  27650  fpwrelmap  28896  xrsclat  29011  cmpcref  29245  sigaex  29499  sigaval  29500  insiga  29527  sigapisys  29545  sigaldsys  29549  measdivcst  29615  ballotlem2  29877  erdszelem7  30433  erdsze2lem2  30440  rellyscon  30487  dffr5  30896  neibastop2lem  31525  neibastop3  31527  topmeet  31529  topjoin  31530  neifg  31536  bj-snglss  32151  bj-restpw  32226  dissneqlem  32363  topdifinfeq  32374  heibor1lem  32778  psubspset  34048  psubclsetN  34240  lcdlss  35926  ismrcd1  36279  pw2f1ocnv  36622  filnm  36678  hbtlem6  36718  sdrgacs  36790  elmapintrab  36901  clcnvlem  36949  psshepw  37102  nbuhgr  40565  nbuhgr2vtx1edgblem  40573  submgmacs  41594  setrec2fun  42238