Theorem elpw2 5289

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  elpwi2  5290  axpweq  5306  knatar  7332  dffi3  9382  marypha1lem  9384  r1pwss  9737  rankr1bg  9756  pwwf  9760  unwf  9763  rankval2  9771  uniwf  9772  rankpwi  9776  dfac2a  10083  dfac12lem2  10098  axdc4lem  10408  axdclem  10472  incexclem  15802  rpnnen2lem1  16182  rpnnen2lem2  16183  sadfval  16422  smufval  16447  smupf  16448  vdwapf  16943  prdshom  17430  mreacs  17619  acsfn  17620  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  clatlem  18461  clatlubcl2  18463  clatglbcl2  18465  issubmgm  18629  issubm  18730  issubg  19058  cntzval  19253  sylow1lem2  19529  lsmvalx  19569  pj1fval  19624  issubrng  20456  issubrg  20480  rgspnval  20521  islss  20840  lspval  20881  lspcl  20882  islbs  20983  lbsextlem1  21068  lbsextlem3  21070  lbsextlem4  21071  sraval  21082  ocvval  21576  isobs  21629  islinds  21718  aspval  21782  uncmp  23290  cmpfi  23295  cmpfii  23296  2ndc1stc  23338  1stcrest  23340  hausllycmp  23381  lly1stc  23383  1stckgenlem  23440  txlly  23523  txnlly  23524  tx1stc  23537  basqtop  23598  tgqtop  23599  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  cncfval  24781  cnllycmp  24855  ovolficcss  25370  ovolval  25374  ovolicc2  25423  ismbl  25427  mblsplit  25433  voliunlem3  25453  vitalilem4  25512  vitalilem5  25513  dvfval  25798  dvnfval  25824  cpnfval  25834  plyval  26098  dmarea  26867  wilthlem2  26979  issh  31137  ocval  31209  spanval  31262  hsupval  31263  sshjval  31279  sshjval3  31283  zarcls  33864  zartopn  33865  sigagensiga  34131  dya2iocuni  34274  coinflippv  34475  ballotlemelo  34479  ballotth  34529  erdszelem1  35178  kur14lem9  35201  kur14  35203  cnllysconn  35232  elmpst  35523  mclsrcl  35548  mclsval  35550  icoreresf  37340  cntotbnd  37790  heibor1lem  37803  heibor  37815  isidl  38008  igenval  38055  paddval  39792  pclvalN  39884  polvalN  39899  docavalN  41117  djavalN  41129  dicval  41170  dochval  41345  djhval  41392  lpolconN  41481  elpwbi  42218  elmzpcl  42714  eldiophb  42745  rpnnen3  43021  islssfgi  43061  hbt  43119  elmnc  43125  itgoval  43150  itgocn  43153  elpglem2  49701