Theorem elpw2 5304

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-pw 4563

This theorem is used by:  elpwi2  5305  axpweq  5320  knatar  7357  dffi3  9389  marypha1lem  9391  r1pwss  9754  rankr1bg  9773  pwwf  9777  unwf  9780  rankval2  9788  uniwf  9789  rankpwi  9793  dfac2a  10120  dfac12lem2  10135  axdc4lem  10445  axdclem  10509  incexclem  15897  rpnnen2lem1  16276  rpnnen2lem2  16277  sadfval  16516  smufval  16541  smupf  16542  vdwapf  17038  prdshom  17526  mreacs  17720  acsfn  17721  lubeldm  18413  lubval  18416  glbeldm  18426  glbval  18429  clatlem  18564  clatlubcl2  18566  clatglbcl2  18568  issubmgm  18766  issubm  18867  issubg  19198  cntzval  19397  sylow1lem2  19675  lsmvalx  19715  pj1fval  19770  issubrng  20657  issubrg  20681  rgspnval  20722  islss  21066  lspval  21107  lspcl  21108  islbs  21208  lbsextlem1  21293  lbsextlem3  21295  lbsextlem4  21296  sraval  21307  ocvval  21828  isobs  21881  islinds  21970  aspval  22033  uncmp  23571  cmpfi  23576  cmpfii  23577  2ndc1stc  23619  1stcrest  23621  hausllycmp  23662  lly1stc  23664  1stckgenlem  23721  txlly  23804  txnlly  23805  tx1stc  23818  basqtop  23879  tgqtop  23880  alexsubALTlem3  24217  alexsubALTlem4  24218  alexsubALT  24219  cncfval  25058  cnllycmp  25126  ovolficcss  25639  ovolval  25643  ovolicc2  25692  ismbl  25696  mblsplit  25702  voliunlem3  25722  vitalilem4  25781  vitalilem5  25782  dvfval  26067  dvnfval  26092  cpnfval  26102  plyval  26361  dmarea  27133  wilthlem2  27244  issh  31571  ocval  31643  spanval  31696  hsupval  31697  sshjval  31713  sshjval3  31717  zarcls  34273  zartopn  34274  sigagensiga  34540  dya2iocuni  34682  coinflippv  34883  ballotlemelo  34887  ballotth  34937  rankval2b  35501  r1ssel  35510  erdszelem1  35691  kur14lem9  35714  kur14  35716  cnllysconn  35745  elmpst  36036  mclsrcl  36061  mclsval  36063  ttcwf  37063  icoreresf  38026  cntotbnd  38475  heibor1lem  38488  heibor  38500  isidl  38693  igenval  38740  paddval  40600  pclvalN  40692  polvalN  40707  docavalN  41925  djavalN  41937  dicval  41978  dochval  42153  djhval  42200  lpolconN  42289  elpwbi  43029  elmzpcl  43485  eldiophb  43516  rpnnen3  43787  islssfgi  43827  hbt  43885  elmnc  43891  itgoval  43916  itgocn  43919  elpglem2  50518