Theorem elpw 4459

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

Syntax hints:   ↔ wb 207   ∈ wcel 2081  Vcvv 3437   ⊆ wss 3859  𝒫 cpw 4453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874  df-pw 4455

This theorem is referenced by:  selpw  4460  0elpw  5147  snelpwi  5228  snelpw  5229  prelpw  5230  sspwb  5233  pwssun  5344  xpsspw  5568  knatar  6973  iunpw  7349  ssenen  8538  fissuni  8675  fipreima  8676  fiin  8732  fipwuni  8736  dffi3  8741  marypha1lem  8743  inf3lem6  8942  tz9.12lem3  9064  rankonidlem  9103  r0weon  9284  infpwfien  9334  dfac5lem4  9398  dfac2b  9402  dfac12lem2  9416  enfin2i  9589  isfin1-3  9654  itunitc1  9688  hsmexlem4  9697  hsmexlem5  9698  axdc4lem  9723  pwfseqlem1  9926  eltsk2g  10019  ixxssxr  12600  ioof  12685  fzof  12885  hashbclem  13658  incexclem  15024  ramub1lem1  16191  ramub1lem2  16192  prdsplusg  16560  prdsmulr  16561  prdsvsca  16562  submrc  16728  isacs2  16753  isssc  16919  homaf  17119  catcfuccl  17198  catcxpccl  17286  clatl  17555  fpwipodrs  17603  isacs4lem  17607  isacs5lem  17608  dprd2dlem1  18880  ablfac1b  18909  cssval  20508  tgdom  21270  distop  21287  fctop  21296  cctop  21298  ppttop  21299  pptbas  21300  epttop  21301  mretopd  21384  resttopon  21453  dishaus  21674  discmp  21690  cmpsublem  21691  cmpsub  21692  conncompid  21723  2ndcsep  21751  cldllycmp  21787  dislly  21789  iskgen3  21841  kgencn2  21849  txuni2  21857  dfac14  21910  prdstopn  21920  txcmplem1  21933  txcmplem2  21934  hmphdis  22088  fbssfi  22129  trfbas2  22135  uffixsn  22217  hauspwpwf1  22279  alexsubALTlem2  22340  ustuqtop0  22532  met1stc  22814  restmetu  22863  icccmplem1  23113  icccmplem2  23114  opnmbllem  23885  sqff1o  25441  incistruhgr  26547  upgrbi  26561  umgrbi  26569  upgr1e  26581  umgredg  26606  uspgr1e  26709  uhgrspansubgrlem  26755  eupth2lems  27705  sspval  28191  foresf1o  29957  cmpcref  30731  esumpcvgval  30954  esumcvg  30962  esum2d  30969  pwsiga  31006  difelsiga  31009  sigainb  31012  inelpisys  31030  pwldsys  31033  rossros  31056  measssd  31091  cntnevol  31104  ddemeas  31112  mbfmcnt  31143  br2base  31144  sxbrsigalem0  31146  oms0  31172  probun  31294  coinfliprv  31357  ballotth  31412  cvmcov2  32131  satfvel  32268  elfuns  32986  altxpsspw  33048  elhf2  33246  neibastop1  33317  neibastop2lem  33318  ctbssinf  34237  opnmbllem0  34478  heiborlem1  34640  heiborlem8  34647  pclfinN  36586  mapd1o  38334  elrfi  38795  ismrcd2  38800  istopclsd  38801  mrefg2  38808  isnacs3  38811  dfac11  39166  islssfg2  39175  lnr2i  39220  clsk1independent  39900  isotone1  39902  isotone2  39903  gneispace  39988  trsspwALT  40710  trsspwALT2  40711  trsspwALT3  40712  pwtrVD  40716  icof  41041  stoweidlem57  41904  intsal  42175  salexct  42179  sge0resplit  42250  sge0reuz  42291  omeiunltfirp  42363  smfpimbor1lem1  42635  sprvalpw  43144  sprsymrelf  43159  sprsymrelf1  43160  prprvalpw  43179  uspgropssxp  43521  uspgrsprf  43523