Theorem elpw 2408

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47.

Hypothesis

Ref	Expression
elpw.1	|- A e. V

Assertion

Ref	Expression
elpw	|- (A e. P~B <-> A (_ B)

Proof of Theorem elpw

Step	Hyp	Ref	Expression
1		elpw.1	. 2 |- A e. V
2		eleq1 1537	. 2 |- (x = A -> (x e. P~B <-> A e. P~B))
3		sseq1 2085	. 2 |- (x = A -> (x (_ B <-> A (_ B))
4		df-pw 2406	. . 3 |- P~B = {x | x (_ B}
5	4	abeq2i 1573	. 2 |- (x e. P~B <-> x (_ B)
6	1, 2, 3, 5	vtoclb 1848	1 |- (A e. P~B <-> A (_ B)

Syntax hints:   <-> wb 146   e. wcel 960  Vcvv 1814   (_ wss 2050  P~cpw 2405

This theorem is referenced by:  elpwg 2409  hbpw 2411  pwid 2412  prsspw 2484  pwv 2506  iinpw 2622  iunpwss 2623  dftr4 2690  0elpw 2741  abssexg 2753  snelpw 2758  sspwb 2761  unipw 2762  pwuni 2763  ssextss 2768  pwin 2831  pwunss 2832  pwssun 2833  pwundif 2834  iunpw 2920  ordpwsuc 3072  xpsspw 3263  fabexg 3659  abexssex 3878  canth 3913  mapval2 4341  pw2en 4452  ssenen 4510  inf3lem6 4627  setind2 4659  r1tr 4664  tz9.12lem3 4671  rankel 4690  rankval3 4691  rankpw 4694  numthlem 4793  ioof 6401  iccf 6402  infxpidmlem9 7561  infmap2lem2 7582  tgval2t 7616  tgss3t 7637  basgent 7639  distop 7646  ntrfval 7664  clsfval 7665  ntrval 7673  clsval 7674  neifval 7711  neif 7712  neival 7714  lpfval 7739  lpval 7740  islp2 7744  lmfval 7922  iscau 7933  sspval 8378  ubthlem6 8530  abfi 10443  ficli 10462  fiv 10470  qusp 10541  fgsb 10555  fgsb2 10560  sfvlim 10576  blkssatm 10738

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056  df-pw 2406

Copyright terms: Public domain