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

Theorem uniexb 4600
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 4554 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4243 . . 3  |-  A  C_  ~P U. A
3 pwexg 4231 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4197 . . 3  |-  ( ( A  C_  ~P U. A  /\  ~P U. A  e. 
_V )  ->  A  e.  _V )
52, 3, 4sylancr 644 . 2  |-  ( U. A  e.  _V  ->  A  e.  _V )
61, 5impbii 180 1  |-  ( A  e.  _V  <->  U. A  e. 
_V )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1701   _Vcvv 2822    C_ wss 3186   ~Pcpw 3659   U.cuni 3864
This theorem is referenced by:  pwexb  4601  ssonprc  4620  ixpexg  6883  rankuni  7580  ac5num  7708  unialeph  7773  ttukeylem1  8181  eltopspOLD  16712  tgss2  16781  ordtbas2  16977  ordtbas  16978  ordttopon  16979  ordtopn1  16980  ordtopn2  16981  ordtrest2  16990  txbasex  17317  ptbasin2  17329  ordthmeolem  17548  alexsublem  17790  alexsub  17791  alexsubb  17792  ussid  23457  brbigcup  24823  isfne  25417  isfne4  25418  isfne4b  25419  isref  25428  fnessref  25442  islocfin  25445  neibastop1  25457  fnejoin2  25467  prtex  25896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-pow 4225  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-v 2824  df-in 3193  df-ss 3200  df-pw 3661  df-uni 3865
  Copyright terms: Public domain W3C validator