Theorem elpw 4607

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  velpw  4608  0elpw  5355  snelpwiOLD  5445  prelpw  5447  sspwb  5450  pwssun  5572  xpsspw  5810  knatar  7354  iunpw  7758  ssenen  9151  fissuni  9357  fipreima  9358  fipwuni  9421  dffi3  9426  marypha1lem  9428  inf3lem6  9628  tz9.12lem3  9784  rankonidlem  9823  r0weon  10007  infpwfien  10057  dfac5lem4  10121  dfac2b  10125  dfac12lem2  10139  enfin2i  10316  isfin1-3  10381  itunitc1  10415  hsmexlem4  10424  hsmexlem5  10425  axdc4lem  10450  pwfseqlem1  10653  eltsk2g  10746  ixxssxr  13336  ioof  13424  fzof  13629  hashbclem  14411  incexclem  15782  ramub1lem1  16959  ramub1lem2  16960  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  submrc  17572  isacs2  17597  isssc  17767  homaf  17980  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  clatl  18461  isacs4lem  18497  isacs5lem  18498  dprd2dlem1  19911  ablfac1b  19940  cssval  21235  tgdom  22481  distop  22498  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  epttop  22512  mretopd  22596  resttopon  22665  dishaus  22886  discmp  22902  cmpsublem  22903  cmpsub  22904  conncompid  22935  2ndcsep  22963  cldllycmp  22999  dislly  23001  iskgen3  23053  kgencn2  23061  txuni2  23069  dfac14  23122  prdstopn  23132  txcmplem1  23145  txcmplem2  23146  hmphdis  23300  fbssfi  23341  trfbas2  23347  uffixsn  23429  hauspwpwf1  23491  alexsubALTlem2  23552  ustuqtop0  23745  met1stc  24030  restmetu  24079  icccmplem1  24338  icccmplem2  24339  opnmbllem  25118  sqff1o  26686  0slt1s  27330  oldf  27352  newf  27353  leftf  27360  rightf  27361  incistruhgr  28339  upgrbi  28353  umgrbi  28361  upgr1e  28373  umgredg  28398  uspgr1e  28501  uhgrspansubgrlem  28547  eupth2lems  29491  sspval  29976  foresf1o  31742  cmpcref  32830  esumpcvgval  33076  esumcvg  33084  esum2d  33091  pwsiga  33128  difelsiga  33131  sigainb  33134  pwldsys  33155  rossros  33178  measssd  33213  cntnevol  33226  ddemeas  33234  mbfmcnt  33267  br2base  33268  sxbrsigalem0  33270  oms0  33296  probun  33418  coinfliprv  33481  ballotth  33536  cvmcov2  34266  satfvel  34403  elfuns  34887  altxpsspw  34949  elhf2  35147  neibastop1  35244  neibastop2lem  35245  ctbssinf  36287  opnmbllem0  36524  heiborlem1  36679  heiborlem8  36686  pclfinN  38771  mapd1o  40519  elrfi  41432  ismrcd2  41437  istopclsd  41438  mrefg2  41445  isnacs3  41448  dfac11  41804  islssfg2  41813  lnr2i  41858  clsk1independent  42797  isotone2  42800  gneispace  42885  ismnushort  43060  trsspwALT  43579  trsspwALT2  43580  trsspwALT3  43581  pwtrVD  43585  icof  43918  stoweidlem57  44773  intsal  45046  salexct  45050  sge0resplit  45122  sge0reuz  45163  omeiunltfirp  45235  smfpimbor1lem1  45514  sprvalpw  46148  sprsymrelf  46163  sprsymrelf1  46164  prprvalpw  46183  uspgropssxp  46522  uspgrsprf  46524