Theorem elpw 4584

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931  𝒫 cpw 4580

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ss 3948  df-pw 4582

This theorem is referenced by:  velpw  4585  0elpw  5331  snelpwiOLD  5424  prelpw  5426  sspwb  5429  pwssun  5550  xpsspw  5793  knatar  7355  iunpw  7770  ssenen  9170  fissuni  9374  fipreima  9375  fipwuni  9443  dffi3  9448  marypha1lem  9450  inf3lem6  9652  tz9.12lem3  9808  rankonidlem  9847  r0weon  10031  infpwfien  10081  dfac5lem4  10145  dfac5lem4OLD  10147  dfac2b  10150  dfac12lem2  10164  enfin2i  10340  isfin1-3  10405  itunitc1  10439  hsmexlem4  10448  hsmexlem5  10449  axdc4lem  10474  pwfseqlem1  10677  eltsk2g  10770  ixxssxr  13379  ioof  13469  fzof  13678  hashbclem  14475  incexclem  15857  ramub1lem1  17051  ramub1lem2  17052  prdsplusg  17477  prdsmulr  17478  prdsvsca  17479  submrc  17645  isacs2  17670  isssc  17838  homaf  18048  catcfuccl  18136  catcxpccl  18224  clatl  18523  isacs4lem  18559  isacs5lem  18560  dprd2dlem1  20029  ablfac1b  20058  cssval  21647  tgdom  22921  distop  22938  fctop  22947  cctop  22949  ppttop  22950  pptbas  22951  epttop  22952  mretopd  23035  resttopon  23104  dishaus  23325  discmp  23341  cmpsublem  23342  cmpsub  23343  conncompid  23374  2ndcsep  23402  cldllycmp  23438  dislly  23440  iskgen3  23492  kgencn2  23500  txuni2  23508  dfac14  23561  prdstopn  23571  txcmplem1  23584  txcmplem2  23585  hmphdis  23739  fbssfi  23780  trfbas2  23786  uffixsn  23868  hauspwpwf1  23930  alexsubALTlem2  23991  ustuqtop0  24184  met1stc  24465  restmetu  24514  icccmplem1  24767  icccmplem2  24768  opnmbllem  25559  sqff1o  27149  0slt1s  27798  oldf  27822  newf  27823  leftf  27834  rightf  27835  elons2  28216  onscutlt  28222  onsiso  28226  onaddscl  28231  onmulscl  28232  incistruhgr  29063  upgrbi  29077  umgrbi  29085  upgr1e  29097  umgredg  29122  uspgr1e  29228  uhgrspansubgrlem  29274  eupth2lems  30224  sspval  30709  foresf1o  32490  cmpcref  33886  esumpcvgval  34114  esumcvg  34122  esum2d  34129  pwsiga  34166  difelsiga  34169  sigainb  34172  pwldsys  34193  rossros  34216  measssd  34251  cntnevol  34264  ddemeas  34272  mbfmcnt  34305  br2base  34306  sxbrsigalem0  34308  oms0  34334  probun  34456  coinfliprv  34520  ballotth  34575  cvmcov2  35302  satfvel  35439  elfuns  35938  altxpsspw  36000  elhf2  36198  neibastop1  36382  neibastop2lem  36383  ctbssinf  37429  opnmbllem0  37685  heiborlem1  37840  heiborlem8  37847  pclfinN  39924  mapd1o  41672  elrfi  42692  ismrcd2  42697  istopclsd  42698  mrefg2  42705  isnacs3  42708  dfac11  43061  islssfg2  43070  lnr2i  43115  clsk1independent  44045  isotone2  44048  gneispace  44133  ismnushort  44300  trsspwALT  44817  trsspwALT2  44818  trsspwALT3  44819  pwtrVD  44823  permaxpow  45009  icof  45223  stoweidlem57  46066  intsal  46339  salexct  46343  sge0resplit  46415  sge0reuz  46456  omeiunltfirp  46528  smfpimbor1lem1  46807  sprvalpw  47474  sprsymrelf  47489  sprsymrelf1  47490  prprvalpw  47509  grimuhgr  47880  uspgropssxp  48099  uspgrsprf  48101