Theorem elpw2 5339

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

Syntax hints:   ↔ wb 206   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  elpwi2  5340  axpweq  5356  knatar  7376  dffi3  9468  marypha1lem  9470  r1pwss  9821  rankr1bg  9840  pwwf  9844  unwf  9847  rankval2  9855  uniwf  9856  rankpwi  9860  dfac2a  10167  dfac12lem2  10182  axdc4lem  10492  axdclem  10556  incexclem  15868  rpnnen2lem1  16246  rpnnen2lem2  16247  sadfval  16485  smufval  16510  smupf  16511  vdwapf  17005  prdshom  17513  mreacs  17702  acsfn  17703  lubeldm  18410  lubval  18413  glbeldm  18423  glbval  18426  clatlem  18559  clatlubcl2  18561  clatglbcl2  18563  issubmgm  18727  issubm  18828  issubg  19156  cntzval  19351  sylow1lem2  19631  lsmvalx  19671  pj1fval  19726  issubrng  20563  issubrg  20587  rgspnval  20628  islss  20949  lspval  20990  lspcl  20991  islbs  21092  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  sraval  21191  ocvval  21702  isobs  21757  islinds  21846  aspval  21910  uncmp  23426  cmpfi  23431  cmpfii  23432  2ndc1stc  23474  1stcrest  23476  hausllycmp  23517  lly1stc  23519  1stckgenlem  23576  txlly  23659  txnlly  23660  tx1stc  23673  basqtop  23734  tgqtop  23735  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  cncfval  24927  cnllycmp  25001  ovolficcss  25517  ovolval  25521  ovolicc2  25570  ismbl  25574  mblsplit  25580  voliunlem3  25600  vitalilem4  25659  vitalilem5  25660  dvfval  25946  dvnfval  25972  cpnfval  25982  plyval  26246  dmarea  27014  wilthlem2  27126  issh  31236  ocval  31308  spanval  31361  hsupval  31362  sshjval  31378  sshjval3  31382  zarcls  33834  zartopn  33835  sigagensiga  34121  dya2iocuni  34264  coinflippv  34464  ballotlemelo  34468  ballotth  34518  erdszelem1  35175  kur14lem9  35198  kur14  35200  cnllysconn  35229  elmpst  35520  mclsrcl  35545  mclsval  35547  icoreresf  37334  cntotbnd  37782  heibor1lem  37795  heibor  37807  isidl  38000  igenval  38047  paddval  39780  pclvalN  39872  polvalN  39887  docavalN  41105  djavalN  41117  dicval  41158  dochval  41333  djhval  41380  lpolconN  41469  elpwbi  42247  elmzpcl  42713  eldiophb  42744  rpnnen3  43020  islssfgi  43060  hbt  43118  elmnc  43124  itgoval  43149  itgocn  43152  elpglem2  48942