Theorem elpw2 5273

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

Syntax hints:   ↔ wb 205   ∈ wcel 2110  Vcvv 3431   ⊆ wss 3892  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-pw 4541

This theorem is referenced by:  elpwi2  5274  axpweq  5291  knatar  7224  dffi3  9168  marypha1lem  9170  r1pwss  9543  rankr1bg  9562  pwwf  9566  unwf  9569  rankval2  9577  uniwf  9578  rankpwi  9582  dfac2a  9886  dfac12lem2  9901  axdc4lem  10212  axdclem  10276  incexclem  15546  rpnnen2lem1  15921  rpnnen2lem2  15922  sadfval  16157  smufval  16182  smupf  16183  vdwapf  16671  prdshom  17176  mreacs  17365  acsfn  17366  lubeldm  18069  lubval  18072  glbeldm  18082  glbval  18085  clatlem  18218  clatlubcl2  18220  clatglbcl2  18222  issubm  18440  issubg  18753  cntzval  18925  sylow1lem2  19202  lsmvalx  19242  pj1fval  19298  issubrg  20022  islss  20194  lspval  20235  lspcl  20236  islbs  20336  lbsextlem1  20418  lbsextlem3  20420  lbsextlem4  20421  sraval  20436  ocvval  20870  isobs  20925  islinds  21014  aspval  21075  uncmp  22552  cmpfi  22557  cmpfii  22558  2ndc1stc  22600  1stcrest  22602  hausllycmp  22643  lly1stc  22645  1stckgenlem  22702  txlly  22785  txnlly  22786  tx1stc  22799  basqtop  22860  tgqtop  22861  alexsubALTlem3  23198  alexsubALTlem4  23199  alexsubALT  23200  cncfval  24049  cnllycmp  24117  ovolficcss  24631  ovolval  24635  ovolicc2  24684  ismbl  24688  mblsplit  24694  voliunlem3  24714  vitalilem4  24773  vitalilem5  24774  dvfval  25059  dvnfval  25084  cpnfval  25094  plyval  25352  dmarea  26105  wilthlem2  26216  issh  29566  ocval  29638  spanval  29691  hsupval  29692  sshjval  29708  sshjval3  29712  zarcls  31820  zartopn  31821  sigagensiga  32105  dya2iocuni  32246  coinflippv  32446  ballotlemelo  32450  ballotth  32500  erdszelem1  33149  kur14lem9  33172  kur14  33174  cnllysconn  33203  elmpst  33494  mclsrcl  33519  mclsval  33521  icoreresf  35519  cntotbnd  35950  heibor1lem  35963  heibor  35975  isidl  36168  igenval  36215  paddval  37808  pclvalN  37900  polvalN  37915  docavalN  39133  djavalN  39145  dicval  39186  dochval  39361  djhval  39408  lpolconN  39497  elpwbi  40202  elmzpcl  40545  eldiophb  40576  rpnnen3  40851  islssfgi  40894  hbt  40952  elmnc  40958  itgoval  40983  itgocn  40986  rgspnval  40990  issubmgm  45312  elpglem2  46386