Theorem elpw2 5248

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  axpweq  5265  knatar  7110  dffi3  8895  marypha1lem  8897  r1pwss  9213  rankr1bg  9232  pwwf  9236  unwf  9239  rankval2  9247  uniwf  9248  rankpwi  9252  dfac2a  9555  dfac12lem2  9570  axdc4lem  9877  axdclem  9941  incexclem  15191  rpnnen2lem1  15567  rpnnen2lem2  15568  sadfval  15801  smufval  15826  smupf  15827  vdwapf  16308  prdshom  16740  mreacs  16929  acsfn  16930  lubeldm  17591  lubval  17594  glbeldm  17604  glbval  17607  clatlem  17721  clatlubcl2  17723  clatglbcl2  17725  issubm  17968  issubg  18279  cntzval  18451  sylow1lem2  18724  lsmvalx  18764  pj1fval  18820  issubrg  19535  islss  19706  lspval  19747  lspcl  19748  islbs  19848  lbsextlem1  19930  lbsextlem3  19932  lbsextlem4  19933  sraval  19948  aspval  20102  ocvval  20811  isobs  20864  islinds  20953  uncmp  22011  cmpfi  22016  cmpfii  22017  2ndc1stc  22059  1stcrest  22061  hausllycmp  22102  lly1stc  22104  1stckgenlem  22161  txlly  22244  txnlly  22245  tx1stc  22258  basqtop  22319  tgqtop  22320  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  cncfval  23496  cnllycmp  23560  ovolficcss  24070  ovolval  24074  ovolicc2  24123  ismbl  24127  mblsplit  24133  voliunlem3  24153  vitalilem4  24212  vitalilem5  24213  dvfval  24495  dvnfval  24519  cpnfval  24529  plyval  24783  dmarea  25535  wilthlem2  25646  issh  28985  ocval  29057  spanval  29110  hsupval  29111  sshjval  29127  sshjval3  29131  sigagensiga  31400  dya2iocuni  31541  coinflippv  31741  ballotlemelo  31745  ballotth  31795  erdszelem1  32438  kur14lem9  32461  kur14  32463  cnllysconn  32492  elmpst  32783  mclsrcl  32808  mclsval  32810  icoreresf  34636  cntotbnd  35089  heibor1lem  35102  heibor  35114  isidl  35307  igenval  35354  paddval  36949  pclvalN  37041  polvalN  37056  docavalN  38274  djavalN  38286  dicval  38327  dochval  38502  djhval  38549  lpolconN  38638  elpwbi  39136  elmzpcl  39343  eldiophb  39374  rpnnen3  39649  islssfgi  39692  hbt  39750  elmnc  39756  itgoval  39781  itgocn  39784  rgspnval  39788  issubmgm  44076  elpglem2  44834