Theorem elpw2 4858

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

Syntax hints:   ↔ wb 196   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607  𝒫 cpw 4191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193

This theorem is referenced by:  axpweq  4872  knatar  6647  canth  6648  dffi3  8378  marypha1lem  8380  r1pwss  8685  rankr1bg  8704  pwwf  8708  unwf  8711  rankval2  8719  uniwf  8720  rankpwi  8724  aceq3lem  8981  dfac2a  8990  dfac12lem2  9004  axdc3lem4  9313  axdc4lem  9315  axdclem  9379  grothpw  9686  uzf  11728  ixxf  12223  fzf  12368  incexclem  14612  rpnnen2lem1  14987  rpnnen2lem2  14988  bitsf  15196  sadfval  15221  smufval  15246  smupf  15247  vdwapf  15723  prdsval  16162  prdsds  16171  prdshom  16174  mreacs  16366  acsfn  16367  wunnat  16663  lubeldm  17028  lubval  17031  glbeldm  17041  glbval  17044  clatlem  17158  clatlubcl2  17160  clatglbcl2  17162  issubm  17394  issubg  17641  cntzval  17800  sylow1lem2  18060  lsmvalx  18100  pj1fval  18153  issubrg  18828  islss  18983  lspval  19023  lspcl  19024  islbs  19124  lbsextlem1  19206  lbsextlem3  19208  lbsextlem4  19209  sraval  19224  aspval  19376  ocvfval  20058  ocvval  20059  isobs  20112  islinds  20196  leordtval2  21064  cnpfval  21086  iscnp2  21091  uncmp  21254  cmpfi  21259  cmpfii  21260  2ndc1stc  21302  1stcrest  21304  islly2  21335  hausllycmp  21345  lly1stc  21347  1stckgenlem  21404  xkotf  21436  txlly  21487  txnlly  21488  tx1stc  21501  basqtop  21562  tgqtop  21563  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  sszcld  22667  cncfval  22738  cnllycmp  22802  bndth  22804  ishtpy  22818  ovolficcss  23284  ovolval  23288  ovolicc2  23336  ismbl  23340  mblsplit  23346  voliunlem3  23366  vitalilem4  23425  vitalilem5  23426  dvfval  23706  dvnfval  23730  cpnfval  23740  plyval  23994  dmarea  24729  wilthlem2  24840  issh  28193  ocval  28267  spanval  28320  hsupval  28321  sshjval  28337  sshjval3  28341  fpwrelmap  29636  sigagensiga  30332  dya2iocuni  30473  coinflippv  30673  ballotlemelo  30677  ballotlem2  30678  ballotth  30727  erdszelem1  31299  kur14lem9  31322  kur14  31324  cnllysconn  31353  elmpst  31559  mclsrcl  31584  mclsval  31586  icoreresf  33330  cover2  33638  cntotbnd  33725  heibor1lem  33738  heibor  33750  isidl  33943  igenval  33990  paddval  35402  pclvalN  35494  polvalN  35509  docavalN  36729  djavalN  36741  dicval  36782  dochval  36957  djhval  37004  lpolconN  37093  elmzpcl  37606  eldiophb  37637  rpnnen3  37916  islssfgi  37959  hbt  38017  elmnc  38023  itgoval  38048  itgocn  38051  rgspnval  38055  issubmgm  42114  elpglem2  42783