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 2145  Vcvv 3453   ⊆ wss 3902  𝒫 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-pw 4562

This theorem is used by:  velpw  4565  0elpw  5324  prelpw  5425  sspwb  5428  pwssun  5551  xpsspw  5794  knatar  7364  iunpw  7774  ssenen  9153  fissuni  9328  fipreima  9329  fipwuni  9400  dffi3  9405  marypha1lem  9407  inf3lem6  9616  tz9.12lem3  9775  rankonidlem  9814  r0weon  10019  infpwfien  10069  dfac5lem4  10133  dfac2b  10137  dfac12lem2  10151  enfin2i  10327  isfin1-3  10392  itunitc1  10426  hsmexlem4  10435  hsmexlem5  10436  axdc4lem  10461  pwfseqlem1  10671  eltsk2g  10764  ixxssxr  13414  ioof  13504  fzof  13715  hashbclem  14521  incexclem  15929  ramub1lem1  17124  ramub1lem2  17125  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  submrc  17722  isacs2  17747  isssc  17915  homaf  18125  catcfuccl  18213  catcxpccl  18301  clatl  18602  isacs4lem  18638  isacs5lem  18639  dprd2dlem1  20176  ablfac1b  20205  cssval  21901  tgdom  23209  distop  23226  fctop  23235  cctop  23237  ppttop  23238  pptbas  23239  epttop  23240  mretopd  23323  resttopon  23392  dishaus  23613  discmp  23629  cmpsublem  23630  cmpsub  23631  conncompid  23662  2ndcsep  23691  cldllycmp  23727  dislly  23729  iskgen3  23781  kgencn2  23789  txuni2  23797  dfac14  23850  prdstopn  23860  txcmplem1  23873  txcmplem2  23874  hmphdis  24028  fbssfi  24069  trfbas2  24075  uffixsn  24157  hauspwpwf1  24219  alexsubALTlem2  24280  ustuqtop0  24472  met1stc  24753  restmetu  24802  icccmplem1  25055  icccmplem2  25056  opnmbllem  25835  sqff1o  27426  0lt1s  28085  oldf  28110  newf  28111  leftf  28128  rightf  28129  elons2  28531  oncutlt  28537  oniso  28544  onaddscl  28550  onmulscl  28551  onsbnd  28554  incistruhgr  29544  upgrbi  29558  umgrbi  29566  upgr1e  29578  umgredg  29603  uspgr1e  29712  uhgrspansubgrlem  29758  eupth2lems  30726  sspval  31212  foresf1o  32987  cmpcref  34368  esumpcvgval  34596  esumcvg  34604  esum2d  34611  pwsiga  34648  sigainb  34655  pwldsys  34676  rossros  34699  measssd  34734  cntnevol  34747  ddemeas  34755  mbfmcnt  34787  br2base  34788  sxbrsigalem0  34790  oms0  34816  probun  34938  coinfliprv  35002  ballotth  35057  cvmcov2  35862  satfvel  35999  elfuns  36500  altxpsspw  36565  elhf2  36763  neibastop1  36986  neibastop2lem  36987  ctbssinf  38168  opnmbllem0  38413  heiborlem1  38569  heiborlem8  38576  pclfinN  40781  mapd1o  42529  elrfi  43547  ismrcd2  43552  istopclsd  43553  mrefg2  43560  isnacs3  43563  dfac11  43911  islssfg2  43920  lnr2i  43965  clsk1independent  44894  isotone2  44897  gneispace  44982  ismnushort  45133  trsspwALT  45648  trsspwALT2  45649  trsspwALT3  45650  pwtrVD  45654  permaxpow  45840  icof  46057  stoweidlem57  46893  intsal  47166  salexct  47170  sge0resplit  47242  sge0reuz  47283  omeiunltfirp  47355  smfpimbor1lem1  47634  sprvalpw  48388  sprsymrelf  48403  sprsymrelf1  48404  prprvalpw  48423  grimuhgr  48811  uspgropssxp  49068  uspgrsprf  49070