Theorem elpw 4554

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3902  𝒫 cpw 4550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3919  df-pw 4552

This theorem is referenced by:  velpw  4555  0elpw  5294  prelpw  5387  sspwb  5390  pwssun  5508  xpsspw  5749  knatar  7291  iunpw  7704  ssenen  9064  fissuni  9241  fipreima  9242  fipwuni  9310  dffi3  9315  marypha1lem  9317  inf3lem6  9523  tz9.12lem3  9679  rankonidlem  9718  r0weon  9900  infpwfien  9950  dfac5lem4  10014  dfac5lem4OLD  10016  dfac2b  10019  dfac12lem2  10033  enfin2i  10209  isfin1-3  10274  itunitc1  10308  hsmexlem4  10317  hsmexlem5  10318  axdc4lem  10343  pwfseqlem1  10546  eltsk2g  10639  ixxssxr  13254  ioof  13344  fzof  13553  hashbclem  14356  incexclem  15740  ramub1lem1  16935  ramub1lem2  16936  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  submrc  17531  isacs2  17556  isssc  17724  homaf  17934  catcfuccl  18022  catcxpccl  18110  clatl  18411  isacs4lem  18447  isacs5lem  18448  dprd2dlem1  19953  ablfac1b  19982  cssval  21617  tgdom  22891  distop  22908  fctop  22917  cctop  22919  ppttop  22920  pptbas  22921  epttop  22922  mretopd  23005  resttopon  23074  dishaus  23295  discmp  23311  cmpsublem  23312  cmpsub  23313  conncompid  23344  2ndcsep  23372  cldllycmp  23408  dislly  23410  iskgen3  23462  kgencn2  23470  txuni2  23478  dfac14  23531  prdstopn  23541  txcmplem1  23554  txcmplem2  23555  hmphdis  23709  fbssfi  23750  trfbas2  23756  uffixsn  23838  hauspwpwf1  23900  alexsubALTlem2  23961  ustuqtop0  24153  met1stc  24434  restmetu  24483  icccmplem1  24736  icccmplem2  24737  opnmbllem  25527  sqff1o  27117  0slt1s  27771  oldf  27796  newf  27797  leftf  27808  rightf  27809  elons2  28193  onscutlt  28199  onsiso  28203  onaddscl  28208  onmulscl  28209  incistruhgr  29055  upgrbi  29069  umgrbi  29077  upgr1e  29089  umgredg  29114  uspgr1e  29220  uhgrspansubgrlem  29266  eupth2lems  30213  sspval  30698  foresf1o  32479  cmpcref  33858  esumpcvgval  34086  esumcvg  34094  esum2d  34101  pwsiga  34138  difelsiga  34141  sigainb  34144  pwldsys  34165  rossros  34188  measssd  34223  cntnevol  34236  ddemeas  34244  mbfmcnt  34276  br2base  34277  sxbrsigalem0  34279  oms0  34305  probun  34427  coinfliprv  34491  ballotth  34546  cvmcov2  35307  satfvel  35444  elfuns  35948  altxpsspw  36010  elhf2  36208  neibastop1  36392  neibastop2lem  36393  ctbssinf  37439  opnmbllem0  37695  heiborlem1  37850  heiborlem8  37857  pclfinN  39938  mapd1o  41686  elrfi  42726  ismrcd2  42731  istopclsd  42732  mrefg2  42739  isnacs3  42742  dfac11  43094  islssfg2  43103  lnr2i  43148  clsk1independent  44078  isotone2  44081  gneispace  44166  ismnushort  44333  trsspwALT  44849  trsspwALT2  44850  trsspwALT3  44851  pwtrVD  44855  permaxpow  45041  icof  45255  stoweidlem57  46094  intsal  46367  salexct  46371  sge0resplit  46443  sge0reuz  46484  omeiunltfirp  46556  smfpimbor1lem1  46835  sprvalpw  47510  sprsymrelf  47525  sprsymrelf1  47526  prprvalpw  47545  grimuhgr  47917  uspgropssxp  48174  uspgrsprf  48176