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

Theorem uniexb 7480
 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 7460 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
2 uniexr 7479 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
31, 2impbii 212 1 (𝐴 ∈ V ↔ 𝐴 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2115  Vcvv 3480  ∪ cuni 4824 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-pow 5253  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-pw 4524  df-uni 4825 This theorem is referenced by:  elpwpwel  7483  ixpexg  8482  rankuni  9289  unialeph  9525  ttukeylem1  9929  tgss2  21595  ordtbas2  21799  ordtbas  21800  ordttopon  21801  ordtopn1  21802  ordtopn2  21803  ordtrest2  21812  isref  22117  islocfin  22125  txbasex  22174  ptbasin2  22186  ordthmeolem  22409  alexsublem  22652  alexsub  22653  alexsubb  22654  ussid  22869  ordtrest2NEW  31223  brbigcup  33416  isfne  33744  isfne4  33745  isfne4b  33746  fnessref  33762  neibastop1  33764  fnejoin2  33774  prtex  36121
 Copyright terms: Public domain W3C validator