Theorem pwex 3487

Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)

Hypothesis

Ref	Expression
zfpowcl.1	|- A e. _V

Assertion

Ref	Expression
pwex	|- ~PA e. _V

Proof of Theorem pwex

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 |- A e. _V
2		pweq 3036	. . 3 |- (z = A -> ~Pz = ~PA)
3	2	eleq1d 1963	. 2 |- (z = A -> (~Pz e. _V <-> ~PA e. _V))
4		axpow2 3483	. . . . . 6 |- E.xA.y(y C_ z -> y e. x)
5	4	bm1.3ii 3441	. . . . 5 |- E.xA.y(y e. x <-> y C_ z)
6		abeq2 1999	. . . . . 6 |- (x = {y | y C_ z} <-> A.y(y e. x <-> y C_ z))
7	6	exbii 1398	. . . . 5 |- (E.x x = {y | y C_ z} <-> E.xA.y(y e. x <-> y C_ z))
8	5, 7	mpbir 207	. . . 4 |- E.x x = {y | y C_ z}
9		isset 2296	. . . 4 |- ({y | y C_ z} e. _V <-> E.x x = {y | y C_ z})
10	8, 9	mpbir 207	. . 3 |- {y | y C_ z} e. _V
11		df-pw 3035	. . . 4 |- ~Pz = {y | y C_ z}
12	11	eleq1i 1960	. . 3 |- (~Pz e. _V <-> {y | y C_ z} e. _V)
13	10, 12	mpbir 207	. 2 |- ~Pz e. _V
14	1, 3, 13	vtocl 2339	1 |- ~PA e. _V

Syntax hints:   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032

This theorem is referenced by:  pwexg 3489  snexOLD 3493  pp0ex 3496  ord3ex 3497  abexssex 4848  pw2en 5505  canth2 5548  undefval 5557  ssenen 5598  pwfilem 5660  pwfi 5661  inf3lem7 5725  r1suc 5763  rankpw 5795  r1pw 5797  rankss 5799  rankuni 5809  rankc2 5817  rankxpu 5822  rankxplim 5823  aceq3lem 5894  numthlem 5945  numthcor 5948  alephsucpw 6018  dominf 6052  npex 6243  pnfxr 6660  pnfxrOLD 6661  mnfxr 6662  mnfxrOLD 6663  infxpidmlem9 8829  infmap2lem2 8849  gch-kn 8856  distop 8919  issubg 9425  sspval 9721  axgroth6 10137  shex 10710  hsupval2 10933  issubcat 15193  taralt 15211  alexsublem2 15438  neibastop2lem1 15519  neibastop2lem4 15522  filssufil 15571  heiborlem23 15977  idlval 16161  lubfval 16803  glbfval 16808  plusssfval 17204  ocvfval 17206  csubspset 17208  psubspset 17225  paddfval 17258  polfval 17317  psubclset 17346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-pow 3481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603  df-ss 2605  df-pw 3035

Copyright terms: Public domain