Theorem pwex 4635

Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Hypothesis

Ref	Expression
zfpowcl.1

Assertion

Ref	Expression
pwex

Proof of Theorem pwex

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2
2		pweq 4015	. . 3
3	2	eleq1d 2526	. 2
4		df-pw 4014	. . 3
5		axpow2 4632	. . . . . 6
6	5	bm1.3ii 4576	. . . . 5
7		abeq2 2581	. . . . . 6
8	7	exbii 1667	. . . . 5
9	6, 8	mpbir 209	. . . 4
10	9	issetri 3116	. . 3
11	4, 10	eqeltri 2541	. 2
12	1, 3, 11	vtocl 3161	1

Syntax hints:  <->wb 184  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442  cvv 3109  C_wss 3475  ~Pcpw 4012

This theorem is referenced by:  pwexg  4636  p0ex  4639  pp0ex  4641  ord3ex  4642  abexssex  6782  fnpm  7447  canth2  7690  dffi3  7911  inf3lem7  8072  r1sucg  8208  r1pwOLD  8285  rankuni  8302  rankc2  8310  rankxpu  8315  rankmapu  8317  rankxplim  8318  r0weon  8411  aceq3lem  8522  dfac5lem4  8528  dfac2a  8531  dfac2  8532  dfac8  8536  dfac13  8543  ackbij1lem5  8625  ackbij1lem8  8628  ackbij2lem2  8641  ackbij2lem3  8642  fin23lem17  8739  domtriomlem  8843  dominf  8846  axdc2lem  8849  axdc3lem  8851  numthcor  8895  axdclem2  8921  alephsucpw  8966  dominfac  8969  canthp1lem1  9051  gchac  9080  intwun  9134  wunex2  9137  eltsk2g  9150  inttsk  9173  tskcard  9180  intgru  9213  gruina  9217  axgroth6  9227  npex  9385  axcnex  9545  pnfxr  11350  mnfxr  11352  ixxex  11569  prdsval  14852  prdsds  14861  prdshom  14864  ismre  14987  fnmre  14988  fnmrc  15004  mrcfval  15005  mrisval  15027  mreacs  15055  wunfunc  15268  catcfuccl  15436  catcxpccl  15476  lubfval  15608  glbfval  15621  isacs5lem  15799  issubm  15978  issubg  16201  cntzfval  16358  pmtrfval  16475  sylow1lem2  16619  lsmfval  16658  pj1fval  16712  issubrg  17429  lssset  17580  lspfval  17619  islbs  17722  lbsext  17809  lbsexg  17810  sraval  17822  aspval  17977  ocvfval  18697  cssval  18713  isobs  18751  islinds  18844  istopon  19426  tgdom  19480  fncld  19523  leordtval2  19713  cnpfval  19735  iscnp2  19740  kgenf  20042  xkoopn  20090  xkouni  20100  dfac14  20119  xkoccn  20120  prdstopn  20129  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  isfbas  20330  uzrest  20398  acufl  20418  alexsubALTlem2  20548  tsmsval2  20628  ustfn  20704  ustn0  20723  ishtpy  21472  vitali  22022  sspval  25636  shex  26129  hsupval  26252  fpwrelmap  27556  fpwrelmapffs  27557  isrnsigaOLD  28112  dmvlsiga  28129  eulerpartlem1  28306  eulerpartgbij  28311  eulerpartlemmf  28314  coinflippv  28422  ballotlemoex  28424  kur14lem9  28658  mpstval  28895  mclsrcl  28921  mclsval  28923  heibor1lem  30305  heibor  30317  idlval  30410  mzpclval  30657  eldiophb  30690  rpnnen3  30974  dfac11  31008  rgspnval  31117  usgsizedg  32395  usgsizedgALT  32396  usgsizedgALT2  32397  issubmgm  32477  lincop  33009  bj-snglex  34531  psubspset  35468  paddfval  35521  pclfvalN  35613  polfvalN  35628  psubclsetN  35660  docafvalN  36849  djafvalN  36861  dicval  36903  dochfval  37077  djhfval  37124  islpolN  37210  pwinfi  37749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014