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

Theorem uniexb 7139
 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 (𝐴 ∈ V ↔ 𝐴 ∈ V)

Proof of Theorem uniexb
StepHypRef Expression
1 uniexg 7121 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
2 uniexr 7138 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
31, 2impbii 199 1 (𝐴 ∈ V ↔ 𝐴 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∈ wcel 2139  Vcvv 3340  ∪ cuni 4588 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-pow 4992  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-in 3722  df-ss 3729  df-pw 4304  df-uni 4589 This theorem is referenced by:  ixpexg  8100  rankuni  8901  unialeph  9134  ttukeylem1  9543  tgss2  21013  ordtbas2  21217  ordtbas  21218  ordttopon  21219  ordtopn1  21220  ordtopn2  21221  ordtrest2  21230  isref  21534  islocfin  21542  txbasex  21591  ptbasin2  21603  ordthmeolem  21826  alexsublem  22069  alexsub  22070  alexsubb  22071  ussid  22285  ordtrest2NEW  30299  omsfval  30686  brbigcup  32332  isfne  32661  isfne4  32662  isfne4b  32663  fnessref  32679  neibastop1  32681  fnejoin2  32691  prtex  34687
 Copyright terms: Public domain W3C validator