Theorem elpw 3729

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)

Hypothesis

Ref	Expression
elpw.1	|- A e. _V

Assertion

Ref	Expression
elpw	|- (A e. ~PB <-> A C_ B)

Proof of Theorem elpw

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpw.1	. 2 |- A e. _V
2		sseq1 3293	. 2 |- (x = A -> (x C_ B <-> A C_ B))
3		df-pw 3725	. 2 |- ~PB = {x | x C_ B}
4	1, 2, 3	elab2 2989	1 |- (A e. ~PB <-> A C_ B)

Syntax hints:   <-> wb 176   e. wcel 1710  _Vcvv 2860   C_ wss 3258  ~Pcpw 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260  df-pw 3725

This theorem is referenced by:  elpwg  3730  prsspw  3879  pwpr  3884  pwtp  3885  pwv  3887  sspwuni  4052  iinpw  4055  iunpwss  4056  snelpwg  4115  snelpwi  4117  unipw  4118  sspwb  4119  pwadjoin  4120  elpw1  4145  dfpw2  4328  eqpw1relk  4480  nnadjoinpw  4522  tfinnnlem1  4534  pw1fnf1o  5856  mapexi  6004  mapval2  6019  mapsspm  6022  mapsspw  6023  enpw1pw  6076  enprmaplem5  6081  enprmaplem6  6082