Theorem elpw2 5105

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

Syntax hints:   ↔ wb 198   ∈ wcel 2050  Vcvv 3415   ⊆ wss 3831  𝒫 cpw 4423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-in 3838  df-ss 3845  df-pw 4425

This theorem is referenced by:  axpweq  5119  knatar  6935  dffi3  8692  marypha1lem  8694  r1pwss  9009  rankr1bg  9028  pwwf  9032  unwf  9035  rankval2  9043  uniwf  9044  rankpwi  9048  dfac2a  9351  dfac12lem2  9366  axdc4lem  9677  axdclem  9741  incexclem  15054  rpnnen2lem1  15430  rpnnen2lem2  15431  sadfval  15664  smufval  15689  smupf  15690  vdwapf  16167  prdshom  16599  mreacs  16790  acsfn  16791  lubeldm  17452  lubval  17455  glbeldm  17465  glbval  17468  clatlem  17582  clatlubcl2  17584  clatglbcl2  17586  issubm  17818  issubg  18066  cntzval  18225  sylow1lem2  18488  lsmvalx  18528  pj1fval  18581  issubrg  19261  islss  19431  lspval  19472  lspcl  19473  islbs  19573  lbsextlem1  19655  lbsextlem3  19657  lbsextlem4  19658  sraval  19673  aspval  19825  ocvval  20516  isobs  20569  islinds  20658  uncmp  21718  cmpfi  21723  cmpfii  21724  2ndc1stc  21766  1stcrest  21768  hausllycmp  21809  lly1stc  21811  1stckgenlem  21868  txlly  21951  txnlly  21952  tx1stc  21965  basqtop  22026  tgqtop  22027  alexsubALTlem3  22364  alexsubALTlem4  22365  alexsubALT  22366  cncfval  23202  cnllycmp  23266  ovolficcss  23776  ovolval  23780  ovolicc2  23829  ismbl  23833  mblsplit  23839  voliunlem3  23859  vitalilem4  23918  vitalilem5  23919  dvfval  24201  dvnfval  24225  cpnfval  24235  plyval  24489  dmarea  25240  wilthlem2  25351  issh  28767  ocval  28841  spanval  28894  hsupval  28895  sshjval  28911  sshjval3  28915  fpwrelmap  30224  sigagensiga  31045  dya2iocuni  31186  coinflippv  31387  ballotlemelo  31391  ballotth  31441  erdszelem1  32023  kur14lem9  32046  kur14  32048  cnllysconn  32077  elmpst  32303  mclsrcl  32328  mclsval  32330  icoreresf  34075  cntotbnd  34516  heibor1lem  34529  heibor  34541  isidl  34734  igenval  34781  paddval  36379  pclvalN  36471  polvalN  36486  docavalN  37704  djavalN  37716  dicval  37757  dochval  37932  djhval  37979  lpolconN  38068  elpwbi  38561  elmzpcl  38718  eldiophb  38749  rpnnen3  39025  islssfgi  39068  hbt  39126  elmnc  39132  itgoval  39157  itgocn  39160  rgspnval  39164  issubmgm  43425  elpglem2  44182