Theorem elpw2 4755

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

Syntax hints:   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  axpweq  4768  knatar  6507  canth  6508  dffi3  8220  marypha1lem  8222  r1pwss  8530  rankr1bg  8549  pwwf  8553  unwf  8556  rankval2  8564  uniwf  8565  rankpwi  8569  aceq3lem  8826  dfac2a  8835  dfac12lem2  8849  axdc3lem4  9158  axdc4lem  9160  axdclem  9224  grothpw  9527  uzf  11566  ixxf  12056  fzf  12201  incexclem  14407  rpnnen2lem1  14782  rpnnen2lem2  14783  bitsf  14987  sadfval  15012  smufval  15037  smupf  15038  vdwapf  15514  prdsval  15938  prdsds  15947  prdshom  15950  mreacs  16142  acsfn  16143  wunnat  16439  lubeldm  16804  lubval  16807  glbeldm  16817  glbval  16820  clatlem  16934  clatlubcl2  16936  clatglbcl2  16938  issubm  17170  issubg  17417  cntzval  17577  sylow1lem2  17837  lsmvalx  17877  pj1fval  17930  issubrg  18603  islss  18756  lspval  18796  lspcl  18797  islbs  18897  lbsextlem1  18979  lbsextlem3  18981  lbsextlem4  18982  sraval  18997  aspval  19149  ocvfval  19829  ocvval  19830  isobs  19883  islinds  19967  leordtval2  20826  cnpfval  20848  iscnp2  20853  uncmp  21016  cmpfi  21021  cmpfii  21022  2ndc1stc  21064  1stcrest  21066  islly2  21097  hausllycmp  21107  lly1stc  21109  1stckgenlem  21166  xkotf  21198  txlly  21249  txnlly  21250  tx1stc  21263  basqtop  21324  tgqtop  21325  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  sszcld  22428  cncfval  22499  cnllycmp  22563  bndth  22565  ishtpy  22579  ovolficcss  23045  ovolval  23049  ovolicc2  23097  ismbl  23101  mblsplit  23107  voliunlem3  23127  vitalilem4  23186  vitalilem5  23187  dvfval  23467  dvnfval  23491  cpnfval  23501  plyval  23753  dmarea  24484  wilthlem2  24595  umgrabi  26510  issh  27449  ocval  27523  spanval  27576  hsupval  27577  sshjval  27593  sshjval3  27597  fpwrelmap  28896  sigagensiga  29531  dya2iocuni  29672  coinflippv  29872  ballotlemelo  29876  ballotlem2  29877  ballotth  29926  erdszelem1  30427  kur14lem9  30450  kur14  30452  cnllyscon  30481  elmpst  30687  mclsrcl  30712  mclsval  30714  icoreresf  32376  cover2  32678  cntotbnd  32765  heibor1lem  32778  heibor  32790  isidl  32983  igenval  33030  paddval  34102  pclvalN  34194  polvalN  34209  docavalN  35430  djavalN  35442  dicval  35483  dochval  35658  djhval  35705  lpolconN  35794  elmzpcl  36307  eldiophb  36338  rpnnen3  36617  islssfgi  36660  hbt  36719  elmnc  36725  itgoval  36750  itgocn  36753  rgspnval  36757  issubmgm  41579  elpglem2  42254