MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniexb Unicode version

Theorem uniexb 4711
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  |-  ( A  e.  _V  <->  U. A  e. 
_V )

Proof of Theorem uniexb
StepHypRef Expression
1 uniexg 4665 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4355 . . 3  |-  A  C_  ~P U. A
3 pwexg 4343 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4309 . . 3  |-  ( ( A  C_  ~P U. A  /\  ~P U. A  e. 
_V )  ->  A  e.  _V )
52, 3, 4sylancr 645 . 2  |-  ( U. A  e.  _V  ->  A  e.  _V )
61, 5impbii 181 1  |-  ( A  e.  _V  <->  U. A  e. 
_V )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   _Vcvv 2916    C_ wss 3280   ~Pcpw 3759   U.cuni 3975
This theorem is referenced by:  pwexb  4712  ssonprc  4731  ixpexg  7045  rankuni  7745  ac5num  7873  unialeph  7938  ttukeylem1  8345  eltopspOLD  16938  tgss2  17007  ordtbas2  17209  ordtbas  17210  ordttopon  17211  ordtopn1  17212  ordtopn2  17213  ordtrest2  17222  txbasex  17551  ptbasin2  17563  ordthmeolem  17786  alexsublem  18028  alexsub  18029  alexsubb  18030  ussid  18243  brbigcup  25652  isfne  26238  isfne4  26239  isfne4b  26240  isref  26249  fnessref  26263  islocfin  26266  neibastop1  26278  fnejoin2  26288  prtex  26619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-pow 4337  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761  df-uni 3976
  Copyright terms: Public domain W3C validator