Theorem elpw2 5301

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

Syntax hints:   ↔ wb 206   ∈ wcel 2107  Vcvv 3457   ⊆ wss 3924  𝒫 cpw 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5263

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-in 3931  df-ss 3941  df-pw 4575

This theorem is referenced by:  elpwi2  5302  axpweq  5318  knatar  7345  dffi3  9437  marypha1lem  9439  r1pwss  9790  rankr1bg  9809  pwwf  9813  unwf  9816  rankval2  9824  uniwf  9825  rankpwi  9829  dfac2a  10136  dfac12lem2  10151  axdc4lem  10461  axdclem  10525  incexclem  15839  rpnnen2lem1  16217  rpnnen2lem2  16218  sadfval  16456  smufval  16481  smupf  16482  vdwapf  16977  prdshom  17466  mreacs  17655  acsfn  17656  lubeldm  18348  lubval  18351  glbeldm  18361  glbval  18364  clatlem  18497  clatlubcl2  18499  clatglbcl2  18501  issubmgm  18665  issubm  18766  issubg  19094  cntzval  19289  sylow1lem2  19565  lsmvalx  19605  pj1fval  19660  issubrng  20492  issubrg  20516  rgspnval  20557  islss  20876  lspval  20917  lspcl  20918  islbs  21019  lbsextlem1  21104  lbsextlem3  21106  lbsextlem4  21107  sraval  21118  ocvval  21612  isobs  21665  islinds  21754  aspval  21818  uncmp  23326  cmpfi  23331  cmpfii  23332  2ndc1stc  23374  1stcrest  23376  hausllycmp  23417  lly1stc  23419  1stckgenlem  23476  txlly  23559  txnlly  23560  tx1stc  23573  basqtop  23634  tgqtop  23635  alexsubALTlem3  23972  alexsubALTlem4  23973  alexsubALT  23974  cncfval  24817  cnllycmp  24891  ovolficcss  25407  ovolval  25411  ovolicc2  25460  ismbl  25464  mblsplit  25470  voliunlem3  25490  vitalilem4  25549  vitalilem5  25550  dvfval  25835  dvnfval  25861  cpnfval  25871  plyval  26135  dmarea  26903  wilthlem2  27015  issh  31121  ocval  31193  spanval  31246  hsupval  31247  sshjval  31263  sshjval3  31267  zarcls  33813  zartopn  33814  sigagensiga  34080  dya2iocuni  34223  coinflippv  34424  ballotlemelo  34428  ballotth  34478  erdszelem1  35134  kur14lem9  35157  kur14  35159  cnllysconn  35188  elmpst  35479  mclsrcl  35504  mclsval  35506  icoreresf  37291  cntotbnd  37741  heibor1lem  37754  heibor  37766  isidl  37959  igenval  38006  paddval  39738  pclvalN  39830  polvalN  39845  docavalN  41063  djavalN  41075  dicval  41116  dochval  41291  djhval  41338  lpolconN  41427  elpwbi  42203  elmzpcl  42674  eldiophb  42705  rpnnen3  42981  islssfgi  43021  hbt  43079  elmnc  43085  itgoval  43110  itgocn  43113  elpglem2  49296