Theorem elpw 4560

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-pw 4558

This theorem is used by:  velpw  4561  0elpw  5316  prelpw  5413  sspwb  5416  pwssun  5542  xpsspw  5786  knatar  7367  iunpw  7785  ssenen  9173  fissuni  9349  fipreima  9350  fipwuni  9421  dffi3  9426  marypha1lem  9428  inf3lem6  9637  tz9.12lem3  9799  rankonidlem  9841  elhf2  9913  r0weon  10094  infpwfien  10144  dfac5lem4  10208  dfac2b  10212  dfac12lem2  10226  enfin2i  10402  isfin1-3  10467  itunitc1  10501  hsmexlem4  10510  hsmexlem5  10511  axdc4lem  10536  pwfseqlem1  10746  eltsk2g  10839  ixxssxr  13491  ioof  13581  fzof  13793  hashbclem  14600  incexclem  16010  ramub1lem1  17209  ramub1lem2  17210  prdsplusg  17634  prdsmulr  17635  prdsvsca  17636  submrc  17807  isacs2  17832  isssc  18000  homaf  18210  catcfuccl  18298  catcxpccl  18386  clatl  18687  isacs4lem  18723  isacs5lem  18724  dprd2dlem1  20262  ablfac1b  20291  cssval  21993  tgdom  23301  distop  23318  fctop  23327  cctop  23329  ppttop  23330  pptbas  23331  epttop  23332  mretopd  23415  resttopon  23484  dishaus  23705  discmp  23721  cmpsublem  23722  cmpsub  23723  conncompid  23754  2ndcsep  23783  cldllycmp  23819  dislly  23821  iskgen3  23873  kgencn2  23881  txuni2  23889  dfac14  23942  prdstopn  23952  txcmplem1  23965  txcmplem2  23966  hmphdis  24120  fbssfi  24161  trfbas2  24167  uffixsn  24249  hauspwpwf1  24311  alexsubALTlem2  24372  ustuqtop0  24564  met1stc  24845  restmetu  24894  icccmplem1  25147  icccmplem2  25148  opnmbllem  25927  sqff1o  27514  0lt1s  28203  oldf  28228  newf  28229  leftf  28246  rightf  28247  elons2  28649  oncutlt  28655  oniso  28662  onaddscl  28668  onmulscl  28669  onsbnd  28672  incistruhgr  29662  upgrbi  29676  umgrbi  29684  upgr1e  29696  umgredg  29721  uspgr1e  29830  uhgrspansubgrlem  29876  eupth2lems  30844  sspval  31330  foresf1o  33147  esumpcvgval  34756  esumcvg  34764  esum2d  34771  pwsiga  34808  sigainb  34815  pwldsys  34836  rossros  34859  measssd  34894  cntnevol  34907  ddemeas  34915  mbfmcnt  34946  br2base  34947  sxbrsigalem0  34949  oms0  34975  probun  35097  coinfliprv  35161  ballotth  35216  cvmcov2  36126  satfvel  36263  elfuns  36769  altxpsspw  36834  neibastop1  37239  neibastop2lem  37240  ctbssinf  38422  opnmbllem0  38667  heiborlem1  38838  heiborlem8  38845  pclfinN  41050  mapd1o  42798  elrfi  43798  ismrcd2  43803  istopclsd  43804  mrefg2  43811  isnacs3  43814  dfac11  44157  islssfg2  44166  lnr2i  44211  clsk1independent  45139  isotone2  45142  gneispace  45227  ismnushort  45378  trsspwALT  45893  trsspwALT2  45894  trsspwALT3  45895  pwtrVD  45899  permaxpow  46092  icof  46325  stoweidlem57  47160  intsal  47433  salexct  47437  sge0resplit  47509  sge0reuz  47550  omeiunltfirp  47622  smfpimbor1lem1  47901  sprvalpw  48655  sprsymrelf  48670  sprsymrelf1  48671  prprvalpw  48690  grimuhgr  49078  uspgropssxp  49335  uspgrsprf  49337