Theorem elpw 4564

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-pw 4562

This theorem is used by:  velpw  4565  0elpw  5321  prelpw  5418  sspwb  5421  pwssun  5547  xpsspw  5792  knatar  7390  iunpw  7809  ssenen  9198  fissuni  9374  fipreima  9375  fipwuni  9445  dffi3  9450  marypha1lem  9452  inf3lem6  9661  tz9.12lem3  9823  rankonidlem  9865  elhf2  9937  r0weon  10118  infpwfien  10168  dfac5lem4  10232  dfac2b  10236  dfac12lem2  10250  enfin2i  10426  isfin1-3  10491  itunitc1  10525  hsmexlem4  10534  hsmexlem5  10535  axdc4lem  10560  pwfseqlem1  10770  eltsk2g  10863  ixxssxr  13515  ioof  13605  fzof  13817  hashbclem  14624  incexclem  16034  ramub1lem1  17233  ramub1lem2  17234  prdsplusg  17658  prdsmulr  17659  prdsvsca  17660  submrc  17831  isacs2  17856  isssc  18024  homaf  18234  catcfuccl  18322  catcxpccl  18410  clatl  18711  isacs4lem  18747  isacs5lem  18748  dprd2dlem1  20287  ablfac1b  20316  cssval  22018  tgdom  23326  distop  23343  fctop  23352  cctop  23354  ppttop  23355  pptbas  23356  epttop  23357  mretopd  23440  resttopon  23509  dishaus  23730  discmp  23746  cmpsublem  23747  cmpsub  23748  conncompid  23779  2ndcsep  23808  cldllycmp  23844  dislly  23846  iskgen3  23898  kgencn2  23906  txuni2  23914  dfac14  23967  prdstopn  23977  txcmplem1  23990  txcmplem2  23991  hmphdis  24145  fbssfi  24186  trfbas2  24192  uffixsn  24274  hauspwpwf1  24336  alexsubALTlem2  24397  ustuqtop0  24589  met1stc  24870  restmetu  24919  icccmplem1  25172  icccmplem2  25173  opnmbllem  25952  sqff1o  27539  0lt1s  28228  oldf  28253  newf  28254  leftf  28271  rightf  28272  elons2  28674  oncutlt  28680  oniso  28687  onaddscl  28693  onmulscl  28694  onsbnd  28697  incistruhgr  29687  upgrbi  29701  umgrbi  29709  upgr1e  29721  umgredg  29746  uspgr1e  29855  uhgrspansubgrlem  29901  eupth2lems  30869  sspval  31355  foresf1o  33172  esumpcvgval  34780  esumcvg  34788  esum2d  34795  pwsiga  34832  sigainb  34839  pwldsys  34860  rossros  34883  measssd  34918  cntnevol  34931  ddemeas  34939  mbfmcnt  34970  br2base  34971  sxbrsigalem0  34973  oms0  34999  probun  35121  coinfliprv  35185  ballotth  35240  cvmcov2  36207  satfvel  36344  elfuns  36855  altxpsspw  36920  neibastop1  37325  neibastop2lem  37326  ctbssinf  38521  opnmbllem0  38766  heiborlem1  38937  heiborlem8  38944  pclfinN  41149  mapd1o  42897  elrfi  43898  ismrcd2  43903  istopclsd  43904  mrefg2  43911  isnacs3  43914  dfac11  44257  islssfg2  44266  lnr2i  44310  clsk1independent  45238  isotone2  45241  gneispace  45326  ismnushort  45477  trsspwALT  45991  trsspwALT2  45992  trsspwALT3  45993  pwtrVD  45997  permaxpow  46194  icof  46437  stoweidlem57  47272  intsal  47545  salexct  47549  sge0resplit  47621  sge0reuz  47662  omeiunltfirp  47734  smfpimbor1lem1  48013  sprvalpw  48767  sprsymrelf  48782  sprsymrelf1  48783  prprvalpw  48802  grimuhgr  49190  uspgropssxp  49447  uspgrsprf  49449