Theorem elpw 4586

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

Syntax hints:   ↔ wb 206   ∈ wcel 2107  Vcvv 3464   ⊆ wss 3933  𝒫 cpw 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ss 3950  df-pw 4584

This theorem is referenced by:  velpw  4587  0elpw  5338  snelpwiOLD  5431  prelpw  5433  sspwb  5436  pwssun  5557  xpsspw  5801  knatar  7360  iunpw  7774  ssenen  9174  fissuni  9380  fipreima  9381  fipwuni  9449  dffi3  9454  marypha1lem  9456  inf3lem6  9656  tz9.12lem3  9812  rankonidlem  9851  r0weon  10035  infpwfien  10085  dfac5lem4  10149  dfac5lem4OLD  10151  dfac2b  10154  dfac12lem2  10168  enfin2i  10344  isfin1-3  10409  itunitc1  10443  hsmexlem4  10452  hsmexlem5  10453  axdc4lem  10478  pwfseqlem1  10681  eltsk2g  10774  ixxssxr  13382  ioof  13470  fzof  13679  hashbclem  14474  incexclem  15855  ramub1lem1  17047  ramub1lem2  17048  prdsplusg  17479  prdsmulr  17480  prdsvsca  17481  submrc  17647  isacs2  17672  isssc  17840  homaf  18051  catcfuccl  18139  catcxpccl  18227  clatl  18527  isacs4lem  18563  isacs5lem  18564  dprd2dlem1  20034  ablfac1b  20063  cssval  21667  tgdom  22951  distop  22968  fctop  22977  cctop  22979  ppttop  22980  pptbas  22981  epttop  22982  mretopd  23065  resttopon  23134  dishaus  23355  discmp  23371  cmpsublem  23372  cmpsub  23373  conncompid  23404  2ndcsep  23432  cldllycmp  23468  dislly  23470  iskgen3  23522  kgencn2  23530  txuni2  23538  dfac14  23591  prdstopn  23601  txcmplem1  23614  txcmplem2  23615  hmphdis  23769  fbssfi  23810  trfbas2  23816  uffixsn  23898  hauspwpwf1  23960  alexsubALTlem2  24021  ustuqtop0  24214  met1stc  24497  restmetu  24546  icccmplem1  24799  icccmplem2  24800  opnmbllem  25591  sqff1o  27180  0slt1s  27829  oldf  27851  newf  27852  leftf  27859  rightf  27860  elons2  28236  onaddscl  28241  onmulscl  28242  incistruhgr  29043  upgrbi  29057  umgrbi  29065  upgr1e  29077  umgredg  29102  uspgr1e  29208  uhgrspansubgrlem  29254  eupth2lems  30204  sspval  30689  foresf1o  32470  cmpcref  33790  esumpcvgval  34020  esumcvg  34028  esum2d  34035  pwsiga  34072  difelsiga  34075  sigainb  34078  pwldsys  34099  rossros  34122  measssd  34157  cntnevol  34170  ddemeas  34178  mbfmcnt  34211  br2base  34212  sxbrsigalem0  34214  oms0  34240  probun  34362  coinfliprv  34426  ballotth  34481  cvmcov2  35221  satfvel  35358  elfuns  35857  altxpsspw  35919  elhf2  36117  neibastop1  36301  neibastop2lem  36302  ctbssinf  37348  opnmbllem0  37604  heiborlem1  37759  heiborlem8  37766  pclfinN  39843  mapd1o  41591  elrfi  42650  ismrcd2  42655  istopclsd  42656  mrefg2  42663  isnacs3  42666  dfac11  43019  islssfg2  43028  lnr2i  43073  clsk1independent  44004  isotone2  44007  gneispace  44092  ismnushort  44265  trsspwALT  44783  trsspwALT2  44784  trsspwALT3  44785  pwtrVD  44789  icof  45169  stoweidlem57  46017  intsal  46290  salexct  46294  sge0resplit  46366  sge0reuz  46407  omeiunltfirp  46479  smfpimbor1lem1  46758  sprvalpw  47413  sprsymrelf  47428  sprsymrelf1  47429  prprvalpw  47448  grimuhgr  47824  uspgropssxp  48006  uspgrsprf  48008