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

Theorem uniexb 4753
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 4707 . 2  |-  ( A  e.  _V  ->  U. A  e.  _V )
2 pwuni 4396 . . 3  |-  A  C_  ~P U. A
3 pwexg 4384 . . 3  |-  ( U. A  e.  _V  ->  ~P
U. A  e.  _V )
4 ssexg 4350 . . 3  |-  ( ( A  C_  ~P U. A  /\  ~P U. A  e. 
_V )  ->  A  e.  _V )
52, 3, 4sylancr 646 . 2  |-  ( U. A  e.  _V  ->  A  e.  _V )
61, 5impbii 182 1  |-  ( A  e.  _V  <->  U. A  e. 
_V )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1726   _Vcvv 2957    C_ wss 3321   ~Pcpw 3800   U.cuni 4016
This theorem is referenced by:  pwexb  4754  ssonprc  4773  ixpexg  7087  rankuni  7790  ac5num  7918  unialeph  7983  ttukeylem1  8390  eltopspOLD  16984  tgss2  17053  ordtbas2  17256  ordtbas  17257  ordttopon  17258  ordtopn1  17259  ordtopn2  17260  ordtrest2  17269  txbasex  17599  ptbasin2  17611  ordthmeolem  17834  alexsublem  18076  alexsub  18077  alexsubb  18078  ussid  18291  brbigcup  25744  isfne  26349  isfne4  26350  isfne4b  26351  isref  26360  fnessref  26374  islocfin  26377  neibastop1  26389  fnejoin2  26399  prtex  26730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-pow 4378  ax-un 4702
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rex 2712  df-v 2959  df-in 3328  df-ss 3335  df-pw 3802  df-uni 4017
  Copyright terms: Public domain W3C validator