Theorem elpw 4114

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

Syntax hints:   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ 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:  selpw  4115  0elpw  4760  snelpwi  4839  snelpw  4840  prelpw  4841  sspwb  4844  pwssun  4944  xpsspw  5156  knatar  6507  iunpw  6870  ssenen  8019  fissuni  8154  fipreima  8155  fiin  8211  fipwuni  8215  dffi3  8220  marypha1lem  8222  inf3lem6  8413  tz9.12lem3  8535  rankonidlem  8574  r0weon  8718  infpwfien  8768  dfac5lem4  8832  dfac2  8836  dfac12lem2  8849  enfin2i  9026  isfin1-3  9091  itunitc1  9125  hsmexlem4  9134  hsmexlem5  9135  axdc4lem  9160  pwfseqlem1  9359  eltsk2g  9452  ixxssxr  12058  ioof  12142  fzof  12336  hashbclem  13093  incexclem  14407  ramub1lem1  15568  ramub1lem2  15569  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  submrc  16111  isacs2  16137  isssc  16303  homaf  16503  catcfuccl  16582  catcxpccl  16670  clatl  16939  fpwipodrs  16987  isacs4lem  16991  isacs5lem  16992  dprd2dlem1  18263  ablfac1b  18292  cssval  19845  tgdom  20593  distop  20610  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  epttop  20623  mretopd  20706  resttopon  20775  dishaus  20996  discmp  21011  cmpsublem  21012  cmpsub  21013  concompid  21044  2ndcsep  21072  cldllycmp  21108  dislly  21110  iskgen3  21162  kgencn2  21170  txuni2  21178  dfac14  21231  prdstopn  21241  txcmplem1  21254  txcmplem2  21255  hmphdis  21409  fbssfi  21451  trfbas2  21457  uffixsn  21539  hauspwpwf1  21601  alexsubALTlem2  21662  ustuqtop0  21854  met1stc  22136  restmetu  22185  icccmplem1  22433  icccmplem2  22434  opnmbllem  23175  sqff1o  24708  incistruhgr  25746  upgrbi  25760  umgrbi  25767  upgr1e  25779  umgredg  25812  umgra1  25855  uslgra1  25901  usgraedgrnv  25906  usgrarnedg  25913  usgraedg4  25916  usgrares1  25939  cusgrarn  25988  eupath2  26507  sspval  26962  foresf1o  28727  cmpcref  29245  esumpcvgval  29467  esumcvg  29475  esum2d  29482  pwsiga  29520  difelsiga  29523  sigainb  29526  inelpisys  29544  pwldsys  29547  rossros  29570  measssd  29605  cntnevol  29618  ddemeas  29626  mbfmcnt  29657  br2base  29658  sxbrsigalem0  29660  oms0  29686  probun  29808  coinfliprv  29871  ballotth  29926  cvmcov2  30511  elfuns  31192  altxpsspw  31254  elhf2  31452  neibastop1  31524  neibastop2lem  31525  opnmbllem0  32615  heiborlem1  32780  heiborlem8  32787  pclfinN  34204  mapd1o  35955  elrfi  36275  ismrcd2  36280  istopclsd  36281  mrefg2  36288  isnacs3  36291  dfac11  36650  islssfg2  36659  lnr2i  36705  clsk1independent  37364  isotone1  37366  isotone2  37367  gneispace  37452  trsspwALT  38067  trsspwALT2  38068  trsspwALT3  38069  pwtrVD  38081  icof  38406  stoweidlem57  38950  intsal  39224  salexct  39228  sge0resplit  39299  sge0reuz  39340  omeiunltfirp  39409  smfpimbor1lem1  39683  uspgr1e  40470  uhgrspansubgrlem  40514  eupth2lems  41406