Theorem elpw 4164

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 3626	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
3		df-pw 4160	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
4	1, 2, 3	elab2 3354	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  selpw  4165  0elpw  4834  snelpwi  4912  snelpw  4913  prelpw  4914  sspwb  4917  pwssun  5020  xpsspw  5233  knatar  6607  iunpw  6978  ssenen  8134  fissuni  8271  fipreima  8272  fiin  8328  fipwuni  8332  dffi3  8337  marypha1lem  8339  inf3lem6  8530  tz9.12lem3  8652  rankonidlem  8691  r0weon  8835  infpwfien  8885  dfac5lem4  8949  dfac2  8953  dfac12lem2  8966  enfin2i  9143  isfin1-3  9208  itunitc1  9242  hsmexlem4  9251  hsmexlem5  9252  axdc4lem  9277  pwfseqlem1  9480  eltsk2g  9573  ixxssxr  12187  ioof  12271  fzof  12467  hashbclem  13236  incexclem  14568  ramub1lem1  15730  ramub1lem2  15731  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  submrc  16288  isacs2  16314  isssc  16480  homaf  16680  catcfuccl  16759  catcxpccl  16847  clatl  17116  fpwipodrs  17164  isacs4lem  17168  isacs5lem  17169  dprd2dlem1  18440  ablfac1b  18469  cssval  20026  tgdom  20782  distop  20799  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  epttop  20813  mretopd  20896  resttopon  20965  dishaus  21186  discmp  21201  cmpsublem  21202  cmpsub  21203  conncompid  21234  2ndcsep  21262  cldllycmp  21298  dislly  21300  iskgen3  21352  kgencn2  21360  txuni2  21368  dfac14  21421  prdstopn  21431  txcmplem1  21444  txcmplem2  21445  hmphdis  21599  fbssfi  21641  trfbas2  21647  uffixsn  21729  hauspwpwf1  21791  alexsubALTlem2  21852  ustuqtop0  22044  met1stc  22326  restmetu  22375  icccmplem1  22625  icccmplem2  22626  opnmbllem  23369  sqff1o  24908  incistruhgr  25974  upgrbi  25988  umgrbi  25996  upgr1e  26008  umgredg  26033  uspgr1e  26136  uhgrspansubgrlem  26182  eupth2lems  27098  sspval  27578  foresf1o  29343  cmpcref  29917  esumpcvgval  30140  esumcvg  30148  esum2d  30155  pwsiga  30193  difelsiga  30196  sigainb  30199  inelpisys  30217  pwldsys  30220  rossros  30243  measssd  30278  cntnevol  30291  ddemeas  30299  mbfmcnt  30330  br2base  30331  sxbrsigalem0  30333  oms0  30359  probun  30481  coinfliprv  30544  ballotth  30599  cvmcov2  31257  dmscut  31918  elfuns  32022  altxpsspw  32084  elhf2  32282  neibastop1  32354  neibastop2lem  32355  opnmbllem0  33445  heiborlem1  33610  heiborlem8  33617  pclfinN  35186  mapd1o  36937  elrfi  37257  ismrcd2  37262  istopclsd  37263  mrefg2  37270  isnacs3  37273  dfac11  37632  islssfg2  37641  lnr2i  37686  clsk1independent  38344  isotone1  38346  isotone2  38347  gneispace  38432  trsspwALT  39045  trsspwALT2  39046  trsspwALT3  39047  pwtrVD  39059  icof  39411  stoweidlem57  40274  intsal  40548  salexct  40552  sge0resplit  40623  sge0reuz  40664  omeiunltfirp  40733  smfpimbor1lem1  41005  sprvalpw  41730  sprsymrelf  41745  sprsymrelf1  41746  uspgropssxp  41752  uspgrsprf  41754