Theorem elpw 4540

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  velpw  4541  0elpw  5291  prelpw  5392  sspwb  5395  pwssun  5517  xpsspw  5759  knatar  7308  iunpw  7721  ssenen  9086  fissuni  9264  fipreima  9265  fipwuni  9336  dffi3  9341  marypha1lem  9343  inf3lem6  9552  tz9.12lem3  9711  rankonidlem  9750  r0weon  9932  infpwfien  9982  dfac5lem4  10046  dfac5lem4OLD  10048  dfac2b  10051  dfac12lem2  10065  enfin2i  10241  isfin1-3  10306  itunitc1  10340  hsmexlem4  10349  hsmexlem5  10350  axdc4lem  10375  pwfseqlem1  10579  eltsk2g  10672  ixxssxr  13308  ioof  13398  fzof  13608  hashbclem  14412  incexclem  15799  ramub1lem1  16995  ramub1lem2  16996  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  submrc  17592  isacs2  17617  isssc  17785  homaf  17995  catcfuccl  18083  catcxpccl  18171  clatl  18472  isacs4lem  18508  isacs5lem  18509  dprd2dlem1  20016  ablfac1b  20045  cssval  21664  tgdom  22968  distop  22985  fctop  22994  cctop  22996  ppttop  22997  pptbas  22998  epttop  22999  mretopd  23082  resttopon  23151  dishaus  23372  discmp  23388  cmpsublem  23389  cmpsub  23390  conncompid  23421  2ndcsep  23449  cldllycmp  23485  dislly  23487  iskgen3  23539  kgencn2  23547  txuni2  23555  dfac14  23608  prdstopn  23618  txcmplem1  23631  txcmplem2  23632  hmphdis  23786  fbssfi  23827  trfbas2  23833  uffixsn  23915  hauspwpwf1  23977  alexsubALTlem2  24038  ustuqtop0  24230  met1stc  24511  restmetu  24560  icccmplem1  24813  icccmplem2  24814  opnmbllem  25593  sqff1o  27170  0lt1s  27829  oldf  27854  newf  27855  leftf  27872  rightf  27873  elons2  28275  oncutlt  28281  oniso  28288  onaddscl  28294  onmulscl  28295  onsbnd  28298  incistruhgr  29173  upgrbi  29187  umgrbi  29195  upgr1e  29207  umgredg  29232  uspgr1e  29338  uhgrspansubgrlem  29384  eupth2lems  30333  sspval  30819  foresf1o  32599  cmpcref  34041  esumpcvgval  34269  esumcvg  34277  esum2d  34284  pwsiga  34321  difelsiga  34324  sigainb  34327  pwldsys  34348  rossros  34371  measssd  34406  cntnevol  34419  ddemeas  34427  mbfmcnt  34459  br2base  34460  sxbrsigalem0  34462  oms0  34488  probun  34610  coinfliprv  34674  ballotth  34729  cvmcov2  35510  satfvel  35647  elfuns  36148  altxpsspw  36212  elhf2  36410  neibastop1  36594  neibastop2lem  36595  ctbssinf  37775  opnmbllem0  38030  heiborlem1  38185  heiborlem8  38192  pclfinN  40399  mapd1o  42147  elrfi  43150  ismrcd2  43155  istopclsd  43156  mrefg2  43163  isnacs3  43166  dfac11  43514  islssfg2  43523  lnr2i  43568  clsk1independent  44497  isotone2  44500  gneispace  44585  ismnushort  44752  trsspwALT  45268  trsspwALT2  45269  trsspwALT3  45270  pwtrVD  45274  permaxpow  45460  icof  45671  stoweidlem57  46507  intsal  46780  salexct  46784  sge0resplit  46856  sge0reuz  46897  omeiunltfirp  46969  smfpimbor1lem1  47248  sprvalpw  47962  sprsymrelf  47977  sprsymrelf1  47978  prprvalpw  47997  grimuhgr  48385  uspgropssxp  48642  uspgrsprf  48644