Theorem elpw2 5295

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3898  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915  df-pw 4558

This theorem is used by:  elpwi2  5296  axpweq  5311  knatar  7355  dffi3  9401  marypha1lem  9403  r1pwss  9766  rankr1bg  9785  pwwf  9789  unwf  9792  rankval2  9800  uniwf  9801  rankpwi  9805  rankval2b  9808  dfac2a  10179  dfac12lem2  10194  axdc4lem  10504  axdclem  10568  incexclem  15972  rpnnen2lem1  16349  rpnnen2lem2  16350  sadfval  16589  smufval  16614  smupf  16615  vdwapf  17111  prdshom  17599  mreacs  17793  acsfn  17794  lubeldm  18486  lubval  18489  glbeldm  18499  glbval  18502  clatlem  18637  clatlubcl2  18639  clatglbcl2  18641  issubmgm  18852  issubm  18959  issubg  19297  cntzval  19496  sylow1lem2  19774  lsmvalx  19814  pj1fval  19869  issubrng  20760  issubrg  20784  rgspnval  20825  islss  21170  lspval  21211  lspcl  21212  islbs  21312  lbsextlem1  21397  lbsextlem3  21399  lbsextlem4  21400  sraval  21411  ocvval  21934  isobs  21987  islinds  22076  aspval  22141  uncmp  23682  cmpfi  23687  cmpfii  23688  2ndc1stc  23730  1stcrest  23732  hausllycmp  23774  lly1stc  23776  1stckgenlem  23833  txlly  23916  txnlly  23917  tx1stc  23930  basqtop  23991  tgqtop  23992  alexsubALTlem3  24329  alexsubALTlem4  24330  alexsubALT  24331  cncfval  25170  cnllycmp  25238  ovolficcss  25751  ovolval  25755  ovolicc2  25804  ismbl  25808  mblsplit  25814  voliunlem3  25834  vitalilem4  25893  vitalilem5  25894  dvfval  26178  dvnfval  26203  cpnfval  26213  plyval  26472  dmarea  27248  wilthlem2  27359  issh  31743  ocval  31815  spanval  31868  hsupval  31869  sshjval  31885  sshjval3  31889  zarcls  34439  zartopn  34440  sigagensiga  34707  dya2iocuni  34849  coinflippv  35050  ballotlemelo  35054  ballotth  35104  r1ssel  35662  erdszelem1  35877  kur14lem9  35900  kur14  35902  cnllysconn  35931  elmpst  36222  mclsrcl  36247  mclsval  36249  ttcwf  37234  icoreresf  38195  cntotbnd  38650  heibor1lem  38663  heibor  38675  isidl  38868  igenval  38915  paddval  40775  pclvalN  40867  polvalN  40882  docavalN  42100  djavalN  42112  dicval  42153  dochval  42328  djhval  42375  lpolconN  42464  elpwbi  43204  elmzpcl  43675  eldiophb  43706  rpnnen3  43977  islssfgi  44017  hbt  44075  elmnc  44081  itgoval  44106  itgocn  44109  elpglem2  50727