Theorem elpw2 4828

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

Syntax hints:   ↔ wb 196   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  axpweq  4842  knatar  6607  canth  6608  dffi3  8337  marypha1lem  8339  r1pwss  8647  rankr1bg  8666  pwwf  8670  unwf  8673  rankval2  8681  uniwf  8682  rankpwi  8686  aceq3lem  8943  dfac2a  8952  dfac12lem2  8966  axdc3lem4  9275  axdc4lem  9277  axdclem  9341  grothpw  9648  uzf  11690  ixxf  12185  fzf  12330  incexclem  14568  rpnnen2lem1  14943  rpnnen2lem2  14944  bitsf  15149  sadfval  15174  smufval  15199  smupf  15200  vdwapf  15676  prdsval  16115  prdsds  16124  prdshom  16127  mreacs  16319  acsfn  16320  wunnat  16616  lubeldm  16981  lubval  16984  glbeldm  16994  glbval  16997  clatlem  17111  clatlubcl2  17113  clatglbcl2  17115  issubm  17347  issubg  17594  cntzval  17754  sylow1lem2  18014  lsmvalx  18054  pj1fval  18107  issubrg  18780  islss  18935  lspval  18975  lspcl  18976  islbs  19076  lbsextlem1  19158  lbsextlem3  19160  lbsextlem4  19161  sraval  19176  aspval  19328  ocvfval  20010  ocvval  20011  isobs  20064  islinds  20148  leordtval2  21016  cnpfval  21038  iscnp2  21043  uncmp  21206  cmpfi  21211  cmpfii  21212  2ndc1stc  21254  1stcrest  21256  islly2  21287  hausllycmp  21297  lly1stc  21299  1stckgenlem  21356  xkotf  21388  txlly  21439  txnlly  21440  tx1stc  21453  basqtop  21514  tgqtop  21515  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  sszcld  22620  cncfval  22691  cnllycmp  22755  bndth  22757  ishtpy  22771  ovolficcss  23238  ovolval  23242  ovolicc2  23290  ismbl  23294  mblsplit  23300  voliunlem3  23320  vitalilem4  23380  vitalilem5  23381  dvfval  23661  dvnfval  23685  cpnfval  23695  plyval  23949  dmarea  24684  wilthlem2  24795  issh  28065  ocval  28139  spanval  28192  hsupval  28193  sshjval  28209  sshjval3  28213  fpwrelmap  29508  sigagensiga  30204  dya2iocuni  30345  coinflippv  30545  ballotlemelo  30549  ballotlem2  30550  ballotth  30599  erdszelem1  31173  kur14lem9  31196  kur14  31198  cnllysconn  31227  elmpst  31433  mclsrcl  31458  mclsval  31460  icoreresf  33200  cover2  33508  cntotbnd  33595  heibor1lem  33608  heibor  33620  isidl  33813  igenval  33860  paddval  35084  pclvalN  35176  polvalN  35191  docavalN  36412  djavalN  36424  dicval  36465  dochval  36640  djhval  36687  lpolconN  36776  elmzpcl  37289  eldiophb  37320  rpnnen3  37599  islssfgi  37642  hbt  37700  elmnc  37706  itgoval  37731  itgocn  37734  rgspnval  37738  issubmgm  41789  elpglem2  42455