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

Theorem uniexb 4563
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 4517 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4206 . . 3  |-  A  C_  ~P U. A
3 pwexg 4194 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4160 . . 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 1684   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625   U.cuni 3827
This theorem is referenced by:  pwexb  4564  ssonprc  4583  ixpexg  6840  rankuni  7535  ac5num  7663  unialeph  7728  ttukeylem1  8136  eltopspOLD  16656  tgss2  16725  ordtbas2  16921  ordtbas  16922  ordttopon  16923  ordtopn1  16924  ordtopn2  16925  ordtrest2  16934  txbasex  17261  ptbasin2  17273  ordthmeolem  17492  alexsublem  17738  alexsub  17739  alexsubb  17740  brbigcup  24438  isfne  26268  isfne4  26269  isfne4b  26270  isref  26279  fnessref  26293  islocfin  26296  neibastop1  26308  fnejoin2  26318  prtex  26748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-uni 3828
  Copyright terms: Public domain W3C validator