Theorem elpw2 5280

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-in 3909  df-ss 3919  df-pw 4557

This theorem is referenced by:  elpwi2  5281  axpweq  5297  knatar  7306  dffi3  9339  marypha1lem  9341  r1pwss  9701  rankr1bg  9720  pwwf  9724  unwf  9727  rankval2  9735  uniwf  9736  rankpwi  9740  dfac2a  10045  dfac12lem2  10060  axdc4lem  10370  axdclem  10434  incexclem  15764  rpnnen2lem1  16144  rpnnen2lem2  16145  sadfval  16384  smufval  16409  smupf  16410  vdwapf  16905  prdshom  17392  mreacs  17586  acsfn  17587  lubeldm  18279  lubval  18282  glbeldm  18292  glbval  18295  clatlem  18430  clatlubcl2  18432  clatglbcl2  18434  issubmgm  18632  issubm  18733  issubg  19061  cntzval  19255  sylow1lem2  19533  lsmvalx  19573  pj1fval  19628  issubrng  20485  issubrg  20509  rgspnval  20550  islss  20890  lspval  20931  lspcl  20932  islbs  21033  lbsextlem1  21118  lbsextlem3  21120  lbsextlem4  21121  sraval  21132  ocvval  21627  isobs  21680  islinds  21769  aspval  21833  uncmp  23352  cmpfi  23357  cmpfii  23358  2ndc1stc  23400  1stcrest  23402  hausllycmp  23443  lly1stc  23445  1stckgenlem  23502  txlly  23585  txnlly  23586  tx1stc  23599  basqtop  23660  tgqtop  23661  alexsubALTlem3  23998  alexsubALTlem4  23999  alexsubALT  24000  cncfval  24842  cnllycmp  24916  ovolficcss  25431  ovolval  25435  ovolicc2  25484  ismbl  25488  mblsplit  25494  voliunlem3  25514  vitalilem4  25573  vitalilem5  25574  dvfval  25859  dvnfval  25885  cpnfval  25895  plyval  26159  dmarea  26928  wilthlem2  27040  issh  31288  ocval  31360  spanval  31413  hsupval  31414  sshjval  31430  sshjval3  31434  zarcls  34044  zartopn  34045  sigagensiga  34311  dya2iocuni  34453  coinflippv  34654  ballotlemelo  34658  ballotth  34708  rankval2b  35268  r1ssel  35276  erdszelem1  35398  kur14lem9  35421  kur14  35423  cnllysconn  35452  elmpst  35743  mclsrcl  35768  mclsval  35770  icoreresf  37570  cntotbnd  38010  heibor1lem  38023  heibor  38035  isidl  38228  igenval  38275  paddval  40137  pclvalN  40229  polvalN  40244  docavalN  41462  djavalN  41474  dicval  41515  dochval  41690  djhval  41737  lpolconN  41826  elpwbi  42565  elmzpcl  43046  eldiophb  43077  rpnnen3  43352  islssfgi  43392  hbt  43450  elmnc  43456  itgoval  43481  itgocn  43484  elpglem2  50034