Theorem uniexb 6610

Description: The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)

Assertion

Ref	Expression
uniexb

Proof of Theorem uniexb

Step	Hyp	Ref	Expression
1		uniexg 6597	. 2
2		pwuni 4683	. . 3
3		pwexg 4636	. . 3
4		ssexg 4598	. . 3
5	2, 3, 4	sylancr 663	. 2
6	1, 5	impbii 188	1

Syntax hints:  <->wb 184  e.wcel 1818  cvv 3109  C_wss 3475  ~Pcpw 4012  U.cuni 4249

This theorem is referenced by:  pwexb  6611  ssonprc  6627  ixpexg  7513  rankuni  8302  ac5num  8438  unialeph  8503  ttukeylem1  8910  eltopspOLD  19419  tgss2  19489  ordtbas2  19692  ordtbas  19693  ordttopon  19694  ordtopn1  19695  ordtopn2  19696  ordtrest2  19705  isref  20010  islocfin  20018  txbasex  20067  ptbasin2  20079  ordthmeolem  20302  alexsublem  20544  alexsub  20545  alexsubb  20546  ussid  20763  ordtrest2NEW  27905  brbigcup  29548  isfne  30157  isfne4  30158  isfne4b  30159  fnessref  30175  neibastop1  30177  fnejoin2  30187  prtex  30621

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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630  ax-un 6592

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-nfc 2607  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014  df-uni 4250