Theorem elpw 4545

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

Hypothesis

Ref	Expression
elpw.1	⊢ 𝐴 ∈ V

Assertion

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

Proof of Theorem elpw

Step	Hyp	Ref	Expression
1		elpw.1	. 2 ⊢ 𝐴 ∈ V
2		elpwg 4544	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-pw 4543

This theorem is referenced by:  velpw  4546  0elpw  5297  prelpw  5398  sspwb  5401  pwssun  5523  xpsspw  5765  knatar  7312  iunpw  7725  ssenen  9089  fissuni  9267  fipreima  9268  fipwuni  9339  dffi3  9344  marypha1lem  9346  inf3lem6  9554  tz9.12lem3  9713  rankonidlem  9752  r0weon  9934  infpwfien  9984  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  dfac12lem2  10067  enfin2i  10243  isfin1-3  10308  itunitc1  10342  hsmexlem4  10351  hsmexlem5  10352  axdc4lem  10377  pwfseqlem1  10581  eltsk2g  10674  ixxssxr  13310  ioof  13400  fzof  13610  hashbclem  14414  incexclem  15801  ramub1lem1  16997  ramub1lem2  16998  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  submrc  17594  isacs2  17619  isssc  17787  homaf  17997  catcfuccl  18085  catcxpccl  18173  clatl  18474  isacs4lem  18510  isacs5lem  18511  dprd2dlem1  20018  ablfac1b  20047  cssval  21662  tgdom  22943  distop  22960  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  epttop  22974  mretopd  23057  resttopon  23126  dishaus  23347  discmp  23363  cmpsublem  23364  cmpsub  23365  conncompid  23396  2ndcsep  23424  cldllycmp  23460  dislly  23462  iskgen3  23514  kgencn2  23522  txuni2  23530  dfac14  23583  prdstopn  23593  txcmplem1  23606  txcmplem2  23607  hmphdis  23761  fbssfi  23802  trfbas2  23808  uffixsn  23890  hauspwpwf1  23952  alexsubALTlem2  24013  ustuqtop0  24205  met1stc  24486  restmetu  24535  icccmplem1  24788  icccmplem2  24789  opnmbllem  25568  sqff1o  27145  0lt1s  27804  oldf  27829  newf  27830  leftf  27847  rightf  27848  elons2  28250  oncutlt  28256  oniso  28263  onaddscl  28269  onmulscl  28270  onsbnd  28273  incistruhgr  29148  upgrbi  29162  umgrbi  29170  upgr1e  29182  umgredg  29207  uspgr1e  29313  uhgrspansubgrlem  29359  eupth2lems  30308  sspval  30794  foresf1o  32574  cmpcref  33994  esumpcvgval  34222  esumcvg  34230  esum2d  34237  pwsiga  34274  difelsiga  34277  sigainb  34280  pwldsys  34301  rossros  34324  measssd  34359  cntnevol  34372  ddemeas  34380  mbfmcnt  34412  br2base  34413  sxbrsigalem0  34415  oms0  34441  probun  34563  coinfliprv  34627  ballotth  34682  cvmcov2  35457  satfvel  35594  elfuns  36095  altxpsspw  36159  elhf2  36357  neibastop1  36541  neibastop2lem  36542  ctbssinf  37722  opnmbllem0  37977  heiborlem1  38132  heiborlem8  38139  pclfinN  40346  mapd1o  42094  elrfi  43126  ismrcd2  43131  istopclsd  43132  mrefg2  43139  isnacs3  43142  dfac11  43490  islssfg2  43499  lnr2i  43544  clsk1independent  44473  isotone2  44476  gneispace  44561  ismnushort  44728  trsspwALT  45244  trsspwALT2  45245  trsspwALT3  45246  pwtrVD  45250  permaxpow  45436  icof  45648  stoweidlem57  46485  intsal  46758  salexct  46762  sge0resplit  46834  sge0reuz  46875  omeiunltfirp  46947  smfpimbor1lem1  47226  sprvalpw  47940  sprsymrelf  47955  sprsymrelf1  47956  prprvalpw  47975  grimuhgr  48363  uspgropssxp  48620  uspgrsprf  48622