Theorem elpw 4308

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)

Hypothesis

Ref	Expression
elpw.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elpw	⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Proof of Theorem elpw

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpw.1	. 2 ⊢ 𝐴 ∈ V
2		sseq1 3767	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
3		df-pw 4304	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
4	1, 2, 3	elab2 3494	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715  𝒫 cpw 4302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-pw 4304

This theorem is referenced by:  selpw  4309  0elpw  4983  snelpwi  5061  snelpw  5062  prelpw  5063  sspwb  5066  pwssun  5170  xpsspw  5389  knatar  6770  iunpw  7143  ssenen  8299  fissuni  8436  fipreima  8437  fiin  8493  fipwuni  8497  dffi3  8502  marypha1lem  8504  inf3lem6  8703  tz9.12lem3  8825  rankonidlem  8864  r0weon  9025  infpwfien  9075  dfac5lem4  9139  dfac2b  9143  dfac2OLD  9145  dfac12lem2  9158  enfin2i  9335  isfin1-3  9400  itunitc1  9434  hsmexlem4  9443  hsmexlem5  9444  axdc4lem  9469  pwfseqlem1  9672  eltsk2g  9765  ixxssxr  12380  ioof  12464  fzof  12661  hashbclem  13428  incexclem  14767  ramub1lem1  15932  ramub1lem2  15933  prdsplusg  16320  prdsmulr  16321  prdsvsca  16322  submrc  16490  isacs2  16515  isssc  16681  homaf  16881  catcfuccl  16960  catcxpccl  17048  clatl  17317  fpwipodrs  17365  isacs4lem  17369  isacs5lem  17370  dprd2dlem1  18640  ablfac1b  18669  cssval  20228  tgdom  20984  distop  21001  fctop  21010  cctop  21012  ppttop  21013  pptbas  21014  epttop  21015  mretopd  21098  resttopon  21167  dishaus  21388  discmp  21403  cmpsublem  21404  cmpsub  21405  conncompid  21436  2ndcsep  21464  cldllycmp  21500  dislly  21502  iskgen3  21554  kgencn2  21562  txuni2  21570  dfac14  21623  prdstopn  21633  txcmplem1  21646  txcmplem2  21647  hmphdis  21801  fbssfi  21842  trfbas2  21848  uffixsn  21930  hauspwpwf1  21992  alexsubALTlem2  22053  ustuqtop0  22245  met1stc  22527  restmetu  22576  icccmplem1  22826  icccmplem2  22827  opnmbllem  23569  sqff1o  25107  incistruhgr  26173  upgrbi  26187  umgrbi  26195  upgr1e  26207  umgredg  26232  uspgr1e  26335  uhgrspansubgrlem  26381  eupth2lems  27390  sspval  27887  foresf1o  29650  cmpcref  30226  esumpcvgval  30449  esumcvg  30457  esum2d  30464  pwsiga  30502  difelsiga  30505  sigainb  30508  inelpisys  30526  pwldsys  30529  rossros  30552  measssd  30587  cntnevol  30600  ddemeas  30608  mbfmcnt  30639  br2base  30640  sxbrsigalem0  30642  oms0  30668  probun  30790  coinfliprv  30853  ballotth  30908  cvmcov2  31564  dmscut  32224  elfuns  32328  altxpsspw  32390  elhf2  32588  neibastop1  32660  neibastop2lem  32661  opnmbllem0  33758  heiborlem1  33923  heiborlem8  33930  pclfinN  35689  mapd1o  37439  elrfi  37759  ismrcd2  37764  istopclsd  37765  mrefg2  37772  isnacs3  37775  dfac11  38134  islssfg2  38143  lnr2i  38188  clsk1independent  38846  isotone1  38848  isotone2  38849  gneispace  38934  trsspwALT  39547  trsspwALT2  39548  trsspwALT3  39549  pwtrVD  39558  icof  39910  stoweidlem57  40777  intsal  41051  salexct  41055  sge0resplit  41126  sge0reuz  41167  omeiunltfirp  41239  smfpimbor1lem1  41511  sprvalpw  42240  sprsymrelf  42255  sprsymrelf1  42256  uspgropssxp  42262  uspgrsprf  42264