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

Theorem uniexb 6921
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 6908 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
2 pwuni 4859 . . 3 𝐴 ⊆ 𝒫 𝐴
3 pwexg 4810 . . 3 ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V)
4 ssexg 4764 . . 3 ((𝐴 ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → 𝐴 ∈ V)
52, 3, 4sylancr 694 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
61, 5impbii 199 1 (𝐴 ∈ V ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1987  Vcvv 3186  wss 3555  𝒫 cpw 4130   cuni 4402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-pow 4803  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-v 3188  df-in 3562  df-ss 3569  df-pw 4132  df-uni 4403
This theorem is referenced by:  pwexb  6922  ssonprc  6939  ixpexg  7876  rankuni  8670  ac5num  8803  unialeph  8868  ttukeylem1  9275  tgss2  20702  ordtbas2  20905  ordtbas  20906  ordttopon  20907  ordtopn1  20908  ordtopn2  20909  ordtrest2  20918  isref  21222  islocfin  21230  txbasex  21279  ptbasin2  21291  ordthmeolem  21514  alexsublem  21758  alexsub  21759  alexsubb  21760  ussid  21974  ordtrest2NEW  29751  omsfval  30137  brbigcup  31647  isfne  31976  isfne4  31977  isfne4b  31978  fnessref  31994  neibastop1  31996  fnejoin2  32006  bj-restv  32685  prtex  33645
  Copyright terms: Public domain W3C validator