Theorem uniexb 7707

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 7683	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
2		uniexr 7706	. 2 ⊢ (∪ 𝐴 ∈ V → 𝐴 ∈ V)
3	1, 2	impbii 209	1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3438  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pow 5308  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554  df-uni 4862

This theorem is referenced by:  elpwpwel  7710  ixpexg  8858  rankuni  9773  unialeph  10009  ttukeylem1  10417  tgss2  22929  ordtbas2  23133  ordtbas  23134  ordttopon  23135  ordtopn1  23136  ordtopn2  23137  ordtrest2  23146  isref  23451  islocfin  23459  txbasex  23508  ptbasin2  23520  ordthmeolem  23743  alexsublem  23986  alexsub  23987  alexsubb  23988  ussid  24202  ordtrest2NEW  34029  brbigcup  36039  isfne  36482  isfne4  36483  isfne4b  36484  fnessref  36500  neibastop1  36502  fnejoin2  36512  prtex  39079