Theorem elpw 4606

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3948  𝒫 cpw 4602

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 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  velpw  4607  0elpw  5354  snelpwiOLD  5444  prelpw  5446  sspwb  5449  pwssun  5571  xpsspw  5808  knatar  7351  iunpw  7755  ssenen  9148  fissuni  9354  fipreima  9355  fipwuni  9418  dffi3  9423  marypha1lem  9425  inf3lem6  9625  tz9.12lem3  9781  rankonidlem  9820  r0weon  10004  infpwfien  10054  dfac5lem4  10118  dfac2b  10122  dfac12lem2  10136  enfin2i  10313  isfin1-3  10378  itunitc1  10412  hsmexlem4  10421  hsmexlem5  10422  axdc4lem  10447  pwfseqlem1  10650  eltsk2g  10743  ixxssxr  13333  ioof  13421  fzof  13626  hashbclem  14408  incexclem  15779  ramub1lem1  16956  ramub1lem2  16957  prdsplusg  17401  prdsmulr  17402  prdsvsca  17403  submrc  17569  isacs2  17594  isssc  17764  homaf  17977  catcfuccl  18066  catcfucclOLD  18067  catcxpccl  18156  catcxpcclOLD  18157  clatl  18458  isacs4lem  18494  isacs5lem  18495  dprd2dlem1  19906  ablfac1b  19935  cssval  21227  tgdom  22473  distop  22490  fctop  22499  cctop  22501  ppttop  22502  pptbas  22503  epttop  22504  mretopd  22588  resttopon  22657  dishaus  22878  discmp  22894  cmpsublem  22895  cmpsub  22896  conncompid  22927  2ndcsep  22955  cldllycmp  22991  dislly  22993  iskgen3  23045  kgencn2  23053  txuni2  23061  dfac14  23114  prdstopn  23124  txcmplem1  23137  txcmplem2  23138  hmphdis  23292  fbssfi  23333  trfbas2  23339  uffixsn  23421  hauspwpwf1  23483  alexsubALTlem2  23544  ustuqtop0  23737  met1stc  24022  restmetu  24071  icccmplem1  24330  icccmplem2  24331  opnmbllem  25110  sqff1o  26676  0slt1s  27320  oldf  27342  newf  27343  leftf  27350  rightf  27351  incistruhgr  28329  upgrbi  28343  umgrbi  28351  upgr1e  28363  umgredg  28388  uspgr1e  28491  uhgrspansubgrlem  28537  eupth2lems  29481  sspval  29964  foresf1o  31730  cmpcref  32819  esumpcvgval  33065  esumcvg  33073  esum2d  33080  pwsiga  33117  difelsiga  33120  sigainb  33123  pwldsys  33144  rossros  33167  measssd  33202  cntnevol  33215  ddemeas  33223  mbfmcnt  33256  br2base  33257  sxbrsigalem0  33259  oms0  33285  probun  33407  coinfliprv  33470  ballotth  33525  cvmcov2  34255  satfvel  34392  elfuns  34876  altxpsspw  34938  elhf2  35136  neibastop1  35233  neibastop2lem  35234  ctbssinf  36276  opnmbllem0  36513  heiborlem1  36668  heiborlem8  36675  pclfinN  38760  mapd1o  40508  elrfi  41418  ismrcd2  41423  istopclsd  41424  mrefg2  41431  isnacs3  41434  dfac11  41790  islssfg2  41799  lnr2i  41844  clsk1independent  42783  isotone2  42786  gneispace  42871  ismnushort  43046  trsspwALT  43565  trsspwALT2  43566  trsspwALT3  43567  pwtrVD  43571  icof  43904  stoweidlem57  44760  intsal  45033  salexct  45037  sge0resplit  45109  sge0reuz  45150  omeiunltfirp  45222  smfpimbor1lem1  45501  sprvalpw  46135  sprsymrelf  46150  sprsymrelf1  46151  prprvalpw  46170  uspgropssxp  46509  uspgrsprf  46511