Theorem elpw2 5347

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

Syntax hints:   ↔ wb 205   ∈ wcel 2098  Vcvv 3463   ⊆ wss 3945  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3420  df-v 3465  df-in 3952  df-ss 3962  df-pw 4605

This theorem is referenced by:  elpwi2  5348  axpweq  5349  knatar  7362  dffi3  9454  marypha1lem  9456  r1pwss  9807  rankr1bg  9826  pwwf  9830  unwf  9833  rankval2  9841  uniwf  9842  rankpwi  9846  dfac2a  10152  dfac12lem2  10167  axdc4lem  10478  axdclem  10542  incexclem  15814  rpnnen2lem1  16190  rpnnen2lem2  16191  sadfval  16426  smufval  16451  smupf  16452  vdwapf  16940  prdshom  17448  mreacs  17637  acsfn  17638  lubeldm  18344  lubval  18347  glbeldm  18357  glbval  18360  clatlem  18493  clatlubcl2  18495  clatglbcl2  18497  issubmgm  18661  issubm  18759  issubg  19085  cntzval  19276  sylow1lem2  19558  lsmvalx  19598  pj1fval  19653  issubrng  20488  issubrg  20514  islss  20822  lspval  20863  lspcl  20864  islbs  20965  lbsextlem1  21050  lbsextlem3  21052  lbsextlem4  21053  sraval  21064  ocvval  21603  isobs  21658  islinds  21747  aspval  21810  uncmp  23337  cmpfi  23342  cmpfii  23343  2ndc1stc  23385  1stcrest  23387  hausllycmp  23428  lly1stc  23430  1stckgenlem  23487  txlly  23570  txnlly  23571  tx1stc  23584  basqtop  23645  tgqtop  23646  alexsubALTlem3  23983  alexsubALTlem4  23984  alexsubALT  23985  cncfval  24838  cnllycmp  24912  ovolficcss  25428  ovolval  25432  ovolicc2  25481  ismbl  25485  mblsplit  25491  voliunlem3  25511  vitalilem4  25570  vitalilem5  25571  dvfval  25856  dvnfval  25882  cpnfval  25892  plyval  26157  dmarea  26919  wilthlem2  27031  issh  31074  ocval  31146  spanval  31199  hsupval  31200  sshjval  31216  sshjval3  31220  zarcls  33545  zartopn  33546  sigagensiga  33830  dya2iocuni  33973  coinflippv  34173  ballotlemelo  34177  ballotth  34227  erdszelem1  34871  kur14lem9  34894  kur14  34896  cnllysconn  34925  elmpst  35216  mclsrcl  35241  mclsval  35243  icoreresf  36901  cntotbnd  37339  heibor1lem  37352  heibor  37364  isidl  37557  igenval  37604  paddval  39340  pclvalN  39432  polvalN  39447  docavalN  40665  djavalN  40677  dicval  40718  dochval  40893  djhval  40940  lpolconN  41029  elpwbi  41787  elmzpcl  42211  eldiophb  42242  rpnnen3  42518  islssfgi  42561  hbt  42619  elmnc  42625  itgoval  42650  itgocn  42653  rgspnval  42657  elpglem2  48255