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

Theorem uniexb 6605
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 6592 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4684 . . 3  |-  A  C_  ~P U. A
3 pwexg 4637 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4599 . . 3  |-  ( ( A  C_  ~P U. A  /\  ~P U. A  e. 
_V )  ->  A  e.  _V )
52, 3, 4sylancr 663 . 2  |-  ( U. A  e.  _V  ->  A  e.  _V )
61, 5impbii 188 1  |-  ( A  e.  _V  <->  U. A  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   _Vcvv 3118    C_ wss 3481   ~Pcpw 4016   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-pow 4631  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2823  df-v 3120  df-in 3488  df-ss 3495  df-pw 4018  df-uni 4252
This theorem is referenced by:  pwexb  6606  ssonprc  6622  ixpexg  7505  rankuni  8293  ac5num  8429  unialeph  8494  ttukeylem1  8901  eltopspOLD  19288  tgss2  19357  ordtbas2  19560  ordtbas  19561  ordttopon  19562  ordtopn1  19563  ordtopn2  19564  ordtrest2  19573  isref  19878  islocfin  19886  txbasex  19935  ptbasin2  19947  ordthmeolem  20170  alexsublem  20412  alexsub  20413  alexsubb  20414  ussid  20631  ordtrest2NEW  27730  brbigcup  29475  isfne  30084  isfne4  30085  isfne4b  30086  fnessref  30102  neibastop1  30104  fnejoin2  30114  prtex  30549
  Copyright terms: Public domain W3C validator