Theorem elpw 4571

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  Vcvv 3458   ⊆ wss 3908  𝒫 cpw 4567

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-pw 4569

This theorem is used by:  velpw  4572  0elpw  5331  prelpw  5432  sspwb  5435  pwssun  5558  xpsspw  5801  knatar  7368  iunpw  7779  ssenen  9149  fissuni  9324  fipreima  9325  fipwuni  9396  dffi3  9401  marypha1lem  9403  inf3lem6  9612  tz9.12lem3  9771  rankonidlem  9810  r0weon  10015  infpwfien  10065  dfac5lem4  10129  dfac2b  10133  dfac12lem2  10147  enfin2i  10323  isfin1-3  10388  itunitc1  10422  hsmexlem4  10431  hsmexlem5  10432  axdc4lem  10457  pwfseqlem1  10661  eltsk2g  10754  ixxssxr  13402  ioof  13492  fzof  13703  hashbclem  14509  incexclem  15916  ramub1lem1  17111  ramub1lem2  17112  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  submrc  17709  isacs2  17734  isssc  17902  homaf  18112  catcfuccl  18200  catcxpccl  18288  clatl  18589  isacs4lem  18625  isacs5lem  18626  dprd2dlem1  20144  ablfac1b  20173  cssval  21869  tgdom  23172  distop  23189  fctop  23198  cctop  23200  ppttop  23201  pptbas  23202  epttop  23203  mretopd  23286  resttopon  23355  dishaus  23576  discmp  23592  cmpsublem  23593  cmpsub  23594  conncompid  23625  2ndcsep  23653  cldllycmp  23689  dislly  23691  iskgen3  23743  kgencn2  23751  txuni2  23759  dfac14  23812  prdstopn  23822  txcmplem1  23835  txcmplem2  23836  hmphdis  23990  fbssfi  24031  trfbas2  24037  uffixsn  24119  hauspwpwf1  24181  alexsubALTlem2  24242  ustuqtop0  24434  met1stc  24715  restmetu  24764  icccmplem1  25017  icccmplem2  25018  opnmbllem  25797  sqff1o  27383  0lt1s  28042  oldf  28067  newf  28068  leftf  28085  rightf  28086  elons2  28488  oncutlt  28494  oniso  28501  onaddscl  28507  onmulscl  28508  onsbnd  28511  incistruhgr  29466  upgrbi  29480  umgrbi  29488  upgr1e  29500  umgredg  29525  uspgr1e  29631  uhgrspansubgrlem  29677  eupth2lems  30626  sspval  31112  foresf1o  32887  cmpcref  34271  esumpcvgval  34499  esumcvg  34507  esum2d  34514  pwsiga  34551  sigainb  34558  pwldsys  34579  rossros  34602  measssd  34637  cntnevol  34650  ddemeas  34658  mbfmcnt  34690  br2base  34691  sxbrsigalem0  34693  oms0  34719  probun  34841  coinfliprv  34905  ballotth  34960  cvmcov2  35788  satfvel  35925  elfuns  36426  altxpsspw  36490  elhf2  36688  neibastop1  36911  neibastop2lem  36912  ctbssinf  38093  opnmbllem0  38348  heiborlem1  38503  heiborlem8  38510  pclfinN  40715  mapd1o  42463  elrfi  43466  ismrcd2  43471  istopclsd  43472  mrefg2  43479  isnacs3  43482  dfac11  43830  islssfg2  43839  lnr2i  43884  clsk1independent  44813  isotone2  44816  gneispace  44901  ismnushort  45052  trsspwALT  45567  trsspwALT2  45568  trsspwALT3  45569  pwtrVD  45573  permaxpow  45759  icof  45976  stoweidlem57  46812  intsal  47085  salexct  47089  sge0resplit  47161  sge0reuz  47202  omeiunltfirp  47274  smfpimbor1lem1  47553  sprvalpw  48270  sprsymrelf  48285  sprsymrelf1  48286  prprvalpw  48305  grimuhgr  48693  uspgropssxp  48950  uspgrsprf  48952