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

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

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