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

Theorem uniexb 7785
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 7761 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
2 uniexr 7784 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
31, 2impbii 209 1 (𝐴 ∈ V ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2107  Vcvv 3479   cuni 4906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-pow 5364  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-in 3957  df-ss 3967  df-pw 4601  df-uni 4907
This theorem is referenced by:  elpwpwel  7788  ixpexg  8963  rankuni  9904  unialeph  10142  ttukeylem1  10550  tgss2  22995  ordtbas2  23200  ordtbas  23201  ordttopon  23202  ordtopn1  23203  ordtopn2  23204  ordtrest2  23213  isref  23518  islocfin  23526  txbasex  23575  ptbasin2  23587  ordthmeolem  23810  alexsublem  24053  alexsub  24054  alexsubb  24055  ussid  24270  ordtrest2NEW  33923  brbigcup  35900  isfne  36341  isfne4  36342  isfne4b  36343  fnessref  36359  neibastop1  36361  fnejoin2  36371  prtex  38882
  Copyright terms: Public domain W3C validator