Theorem elpw 2400

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 1531	. 2 |- (x = A -> (x e. P~B <-> A e. P~B))
3		sseq1 2078	. 2 |- (x = A -> (x (_ B <-> A (_ B))
4		df-pw 2398	. . 3 |- P~B = {x | x (_ B}
5	4	abeq2i 1567	. 2 |- (x e. P~B <-> x (_ B)
6	1, 2, 3, 5	vtoclb 1841	1 |- (A e. P~B <-> A (_ B)

Syntax hints:   <-> wb 146   e. wcel 956  Vcvv 1807   (_ wss 2043  P~cpw 2397

This theorem is referenced by:  elpwg 2401  hbpw 2403  pwid 2404  prsspw 2476  pwv 2497  iinpw 2612  iunpwss 2613  dftr4 2680  0elpw 2731  abssexg 2742  snelpw 2747  sspwb 2750  unipw 2751  pwuni 2752  ssextss 2757  pwin 2820  pwunss 2821  pwssun 2822  pwundif 2823  iunpw 2909  ordpwsuc 3061  xpsspw 3252  fabexg 3644  abexssex 3863  canth 3898  mapval2 4325  pw2en 4432  ssenen 4490  inf3lem6 4598  setind2 4629  r1tr 4634  tz9.12lem3 4641  rankel 4660  rankval3 4661  rankpw 4664  numthlem 4763  ioof 6341  iccf 6342  infxpidmlem9 7511  infmap2lem2 7530  tgval2t 7567  tgss3t 7588  basgent 7590  distop 7599  ntrfval 7617  clsfval 7618  ntrval 7626  clsval 7627  neifval 7664  neif 7665  neival 7667  lpfval 7692  lpval 7693  islp2 7697  lmfval 7877  iscau 7888  sspval 8329  ubthlem6 8478  abfi 10385  ficli 10404  fiv 10410  qusp 10466  fgsb 10480  fgsb2 10485  dtopcl 10495  blkssatm 10639

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-pw 2398

Copyright terms: Public domain