Theorem elpw2g 2732

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

Assertion

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

Proof of Theorem elpw2g

Step	Hyp	Ref	Expression
1		elpwi 2410	. 2 |- (A e. P~B -> A (_ B)
2		ssexg 2726	. . . 4 |- ((A (_ B /\ B e. C) -> A e. V)
3		elpwg 2409	. . . . 5 |- (A e. V -> (A e. P~B <-> A (_ B))
4	3	biimparc 421	. . . 4 |- ((A (_ B /\ A e. V) -> A e. P~B)
5	2, 4	syldan 469	. . 3 |- ((A (_ B /\ B e. C) -> A e. P~B)
6	5	expcom 374	. 2 |- (B e. C -> (A (_ B -> A e. P~B))
7	1, 6	impbid2 520	1 |- (B e. C -> (A e. P~B <-> A (_ B))

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

This theorem is referenced by:  elpw2 2733  cncfval 7264  uniopnt 7599  ntrval 7673  clsval 7674  neiss2 7713  neival 7714  lpval 7740  islp2 7744  blf 7841  iscau 7933  ump 10449  fillsb 10546  filint2 10557  efilcp2 10561  rcfpfil 10569

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  ax-sep 2708

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