Theorem uniexb 7700

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

Step	Hyp	Ref	Expression
1		uniexg 7676	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
2		uniexr 7699	. 2 ⊢ (∪ 𝐴 ∈ V → 𝐴 ∈ V)
3	1, 2	impbii 209	1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3436  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pow 5304  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553  df-uni 4859

This theorem is referenced by:  elpwpwel  7703  ixpexg  8849  rankuni  9759  unialeph  9995  ttukeylem1  10403  tgss2  22872  ordtbas2  23076  ordtbas  23077  ordttopon  23078  ordtopn1  23079  ordtopn2  23080  ordtrest2  23089  isref  23394  islocfin  23402  txbasex  23451  ptbasin2  23463  ordthmeolem  23686  alexsublem  23929  alexsub  23930  alexsubb  23931  ussid  24146  ordtrest2NEW  33890  brbigcup  35876  isfne  36317  isfne4  36318  isfne4b  36319  fnessref  36335  neibastop1  36337  fnejoin2  36347  prtex  38863