Theorem elpw2 5352

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  elpwi2  5353  axpweq  5369  knatar  7393  dffi3  9500  marypha1lem  9502  r1pwss  9853  rankr1bg  9872  pwwf  9876  unwf  9879  rankval2  9887  uniwf  9888  rankpwi  9892  dfac2a  10199  dfac12lem2  10214  axdc4lem  10524  axdclem  10588  incexclem  15884  rpnnen2lem1  16262  rpnnen2lem2  16263  sadfval  16498  smufval  16523  smupf  16524  vdwapf  17019  prdshom  17527  mreacs  17716  acsfn  17717  lubeldm  18423  lubval  18426  glbeldm  18436  glbval  18439  clatlem  18572  clatlubcl2  18574  clatglbcl2  18576  issubmgm  18740  issubm  18838  issubg  19166  cntzval  19361  sylow1lem2  19641  lsmvalx  19681  pj1fval  19736  issubrng  20573  issubrg  20599  islss  20955  lspval  20996  lspcl  20997  islbs  21098  lbsextlem1  21183  lbsextlem3  21185  lbsextlem4  21186  sraval  21197  ocvval  21708  isobs  21763  islinds  21852  aspval  21916  uncmp  23432  cmpfi  23437  cmpfii  23438  2ndc1stc  23480  1stcrest  23482  hausllycmp  23523  lly1stc  23525  1stckgenlem  23582  txlly  23665  txnlly  23666  tx1stc  23679  basqtop  23740  tgqtop  23741  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  cncfval  24933  cnllycmp  25007  ovolficcss  25523  ovolval  25527  ovolicc2  25576  ismbl  25580  mblsplit  25586  voliunlem3  25606  vitalilem4  25665  vitalilem5  25666  dvfval  25952  dvnfval  25978  cpnfval  25988  plyval  26252  dmarea  27018  wilthlem2  27130  issh  31240  ocval  31312  spanval  31365  hsupval  31366  sshjval  31382  sshjval3  31386  zarcls  33820  zartopn  33821  sigagensiga  34105  dya2iocuni  34248  coinflippv  34448  ballotlemelo  34452  ballotth  34502  erdszelem1  35159  kur14lem9  35182  kur14  35184  cnllysconn  35213  elmpst  35504  mclsrcl  35529  mclsval  35531  icoreresf  37318  cntotbnd  37756  heibor1lem  37769  heibor  37781  isidl  37974  igenval  38021  paddval  39755  pclvalN  39847  polvalN  39862  docavalN  41080  djavalN  41092  dicval  41133  dochval  41308  djhval  41355  lpolconN  41444  elpwbi  42223  elmzpcl  42682  eldiophb  42713  rpnnen3  42989  islssfgi  43029  hbt  43087  elmnc  43093  itgoval  43118  itgocn  43121  rgspnval  43125  elpglem2  48804