Theorem elpw 4626

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  velpw  4627  0elpw  5374  snelpwiOLD  5464  prelpw  5466  sspwb  5469  pwssun  5590  xpsspw  5833  knatar  7393  iunpw  7806  ssenen  9217  fissuni  9427  fipreima  9428  fipwuni  9495  dffi3  9500  marypha1lem  9502  inf3lem6  9702  tz9.12lem3  9858  rankonidlem  9897  r0weon  10081  infpwfien  10131  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  dfac12lem2  10214  enfin2i  10390  isfin1-3  10455  itunitc1  10489  hsmexlem4  10498  hsmexlem5  10499  axdc4lem  10524  pwfseqlem1  10727  eltsk2g  10820  ixxssxr  13419  ioof  13507  fzof  13713  hashbclem  14501  incexclem  15884  ramub1lem1  17073  ramub1lem2  17074  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  submrc  17686  isacs2  17711  isssc  17881  homaf  18097  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  clatl  18578  isacs4lem  18614  isacs5lem  18615  dprd2dlem1  20085  ablfac1b  20114  cssval  21723  tgdom  23006  distop  23023  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  epttop  23037  mretopd  23121  resttopon  23190  dishaus  23411  discmp  23427  cmpsublem  23428  cmpsub  23429  conncompid  23460  2ndcsep  23488  cldllycmp  23524  dislly  23526  iskgen3  23578  kgencn2  23586  txuni2  23594  dfac14  23647  prdstopn  23657  txcmplem1  23670  txcmplem2  23671  hmphdis  23825  fbssfi  23866  trfbas2  23872  uffixsn  23954  hauspwpwf1  24016  alexsubALTlem2  24077  ustuqtop0  24270  met1stc  24555  restmetu  24604  icccmplem1  24863  icccmplem2  24864  opnmbllem  25655  sqff1o  27243  0slt1s  27892  oldf  27914  newf  27915  leftf  27922  rightf  27923  elons2  28299  onaddscl  28304  onmulscl  28305  incistruhgr  29114  upgrbi  29128  umgrbi  29136  upgr1e  29148  umgredg  29173  uspgr1e  29279  uhgrspansubgrlem  29325  eupth2lems  30270  sspval  30755  foresf1o  32532  cmpcref  33796  esumpcvgval  34042  esumcvg  34050  esum2d  34057  pwsiga  34094  difelsiga  34097  sigainb  34100  pwldsys  34121  rossros  34144  measssd  34179  cntnevol  34192  ddemeas  34200  mbfmcnt  34233  br2base  34234  sxbrsigalem0  34236  oms0  34262  probun  34384  coinfliprv  34447  ballotth  34502  cvmcov2  35243  satfvel  35380  elfuns  35879  altxpsspw  35941  elhf2  36139  neibastop1  36325  neibastop2lem  36326  ctbssinf  37372  opnmbllem0  37616  heiborlem1  37771  heiborlem8  37778  pclfinN  39857  mapd1o  41605  elrfi  42650  ismrcd2  42655  istopclsd  42656  mrefg2  42663  isnacs3  42666  dfac11  43019  islssfg2  43028  lnr2i  43073  clsk1independent  44008  isotone2  44011  gneispace  44096  ismnushort  44270  trsspwALT  44789  trsspwALT2  44790  trsspwALT3  44791  pwtrVD  44795  icof  45126  stoweidlem57  45978  intsal  46251  salexct  46255  sge0resplit  46327  sge0reuz  46368  omeiunltfirp  46440  smfpimbor1lem1  46719  sprvalpw  47354  sprsymrelf  47369  sprsymrelf1  47370  prprvalpw  47389  grimuhgr  47762  uspgropssxp  47867  uspgrsprf  47869