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

Theorem uniexb 6385
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 6376 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4522 . . 3  |-  A  C_  ~P U. A
3 pwexg 4475 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4437 . . 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 1756   _Vcvv 2971    C_ wss 3327   ~Pcpw 3859   U.cuni 4090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-pow 4469  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2720  df-v 2973  df-in 3334  df-ss 3341  df-pw 3861  df-uni 4091
This theorem is referenced by:  pwexb  6386  ssonprc  6402  ixpexg  7286  rankuni  8069  ac5num  8205  unialeph  8270  ttukeylem1  8677  eltopspOLD  18522  tgss2  18591  ordtbas2  18794  ordtbas  18795  ordttopon  18796  ordtopn1  18797  ordtopn2  18798  ordtrest2  18807  txbasex  19138  ptbasin2  19150  ordthmeolem  19373  alexsublem  19615  alexsub  19616  alexsubb  19617  ussid  19834  ordtrest2NEW  26352  brbigcup  27928  isfne  28538  isfne4  28539  isfne4b  28540  isref  28549  fnessref  28563  islocfin  28566  neibastop1  28578  fnejoin2  28588  prtex  29023
  Copyright terms: Public domain W3C validator