Theorem elpw 4551

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 4550	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3433   ⊆ wss 3899  𝒫 cpw 4547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3916  df-pw 4549

This theorem is referenced by:  velpw  4552  0elpw  5291  prelpw  5384  sspwb  5387  pwssun  5505  xpsspw  5746  knatar  7285  iunpw  7698  ssenen  9058  fissuni  9235  fipreima  9236  fipwuni  9304  dffi3  9309  marypha1lem  9311  inf3lem6  9517  tz9.12lem3  9673  rankonidlem  9712  r0weon  9894  infpwfien  9944  dfac5lem4  10008  dfac5lem4OLD  10010  dfac2b  10013  dfac12lem2  10027  enfin2i  10203  isfin1-3  10268  itunitc1  10302  hsmexlem4  10311  hsmexlem5  10312  axdc4lem  10337  pwfseqlem1  10540  eltsk2g  10633  ixxssxr  13248  ioof  13338  fzof  13547  hashbclem  14347  incexclem  15730  ramub1lem1  16925  ramub1lem2  16926  prdsplusg  17349  prdsmulr  17350  prdsvsca  17351  submrc  17521  isacs2  17546  isssc  17714  homaf  17924  catcfuccl  18012  catcxpccl  18100  clatl  18401  isacs4lem  18437  isacs5lem  18438  dprd2dlem1  19909  ablfac1b  19938  cssval  21573  tgdom  22847  distop  22864  fctop  22873  cctop  22875  ppttop  22876  pptbas  22877  epttop  22878  mretopd  22961  resttopon  23030  dishaus  23251  discmp  23267  cmpsublem  23268  cmpsub  23269  conncompid  23300  2ndcsep  23328  cldllycmp  23364  dislly  23366  iskgen3  23418  kgencn2  23426  txuni2  23434  dfac14  23487  prdstopn  23497  txcmplem1  23510  txcmplem2  23511  hmphdis  23665  fbssfi  23706  trfbas2  23712  uffixsn  23794  hauspwpwf1  23856  alexsubALTlem2  23917  ustuqtop0  24109  met1stc  24390  restmetu  24439  icccmplem1  24692  icccmplem2  24693  opnmbllem  25483  sqff1o  27073  0slt1s  27727  oldf  27752  newf  27753  leftf  27764  rightf  27765  elons2  28149  onscutlt  28155  onsiso  28159  onaddscl  28164  onmulscl  28165  incistruhgr  29011  upgrbi  29025  umgrbi  29033  upgr1e  29045  umgredg  29070  uspgr1e  29176  uhgrspansubgrlem  29222  eupth2lems  30169  sspval  30654  foresf1o  32436  cmpcref  33831  esumpcvgval  34059  esumcvg  34067  esum2d  34074  pwsiga  34111  difelsiga  34114  sigainb  34117  pwldsys  34138  rossros  34161  measssd  34196  cntnevol  34209  ddemeas  34217  mbfmcnt  34249  br2base  34250  sxbrsigalem0  34252  oms0  34278  probun  34400  coinfliprv  34464  ballotth  34519  cvmcov2  35265  satfvel  35402  elfuns  35906  altxpsspw  35968  elhf2  36166  neibastop1  36350  neibastop2lem  36351  ctbssinf  37397  opnmbllem0  37653  heiborlem1  37808  heiborlem8  37815  pclfinN  39896  mapd1o  41644  elrfi  42684  ismrcd2  42689  istopclsd  42690  mrefg2  42697  isnacs3  42700  dfac11  43052  islssfg2  43061  lnr2i  43106  clsk1independent  44036  isotone2  44039  gneispace  44124  ismnushort  44291  trsspwALT  44807  trsspwALT2  44808  trsspwALT3  44809  pwtrVD  44813  permaxpow  44999  icof  45213  stoweidlem57  46052  intsal  46325  salexct  46329  sge0resplit  46401  sge0reuz  46442  omeiunltfirp  46514  smfpimbor1lem1  46793  sprvalpw  47478  sprsymrelf  47493  sprsymrelf1  47494  prprvalpw  47513  grimuhgr  47885  uspgropssxp  48142  uspgrsprf  48144