Theorem elpw2 5276

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)

Hypothesis

Ref	Expression
elpw2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
elpw2	⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Proof of Theorem elpw2

Step	Hyp	Ref	Expression
1		elpw2.1	. 2 ⊢ 𝐵 ∈ V
2		elpw2g 5275	. 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpwi2  5277  axpweq  5293  knatar  7312  dffi3  9344  marypha1lem  9346  r1pwss  9708  rankr1bg  9727  pwwf  9731  unwf  9734  rankval2  9742  uniwf  9743  rankpwi  9747  dfac2a  10052  dfac12lem2  10067  axdc4lem  10377  axdclem  10441  incexclem  15801  rpnnen2lem1  16181  rpnnen2lem2  16182  sadfval  16421  smufval  16446  smupf  16447  vdwapf  16943  prdshom  17430  mreacs  17624  acsfn  17625  lubeldm  18317  lubval  18320  glbeldm  18330  glbval  18333  clatlem  18468  clatlubcl2  18470  clatglbcl2  18472  issubmgm  18670  issubm  18771  issubg  19102  cntzval  19296  sylow1lem2  19574  lsmvalx  19614  pj1fval  19669  issubrng  20524  issubrg  20548  rgspnval  20589  islss  20929  lspval  20970  lspcl  20971  islbs  21071  lbsextlem1  21156  lbsextlem3  21158  lbsextlem4  21159  sraval  21170  ocvval  21647  isobs  21700  islinds  21789  aspval  21852  uncmp  23368  cmpfi  23373  cmpfii  23374  2ndc1stc  23416  1stcrest  23418  hausllycmp  23459  lly1stc  23461  1stckgenlem  23518  txlly  23601  txnlly  23602  tx1stc  23615  basqtop  23676  tgqtop  23677  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  cncfval  24855  cnllycmp  24923  ovolficcss  25436  ovolval  25440  ovolicc2  25489  ismbl  25493  mblsplit  25499  voliunlem3  25519  vitalilem4  25578  vitalilem5  25579  dvfval  25864  dvnfval  25889  cpnfval  25899  plyval  26158  dmarea  26921  wilthlem2  27032  issh  31279  ocval  31351  spanval  31404  hsupval  31405  sshjval  31421  sshjval3  31425  zarcls  34018  zartopn  34019  sigagensiga  34285  dya2iocuni  34427  coinflippv  34628  ballotlemelo  34632  ballotth  34682  rankval2b  35242  r1ssel  35250  erdszelem1  35373  kur14lem9  35396  kur14  35398  cnllysconn  35427  elmpst  35718  mclsrcl  35743  mclsval  35745  ttcwf  36706  icoreresf  37668  cntotbnd  38117  heibor1lem  38130  heibor  38142  isidl  38335  igenval  38382  paddval  40244  pclvalN  40336  polvalN  40351  docavalN  41569  djavalN  41581  dicval  41622  dochval  41797  djhval  41844  lpolconN  41933  elpwbi  42671  elmzpcl  43158  eldiophb  43189  rpnnen3  43460  islssfgi  43500  hbt  43558  elmnc  43564  itgoval  43589  itgocn  43592  elpglem2  50181