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 210	1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)

Syntax hints:   ↔ wb 207   ∈ wcel 2119  Vcvv 3431  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531  df-uni 4839

This theorem is referenced by:  elpwpwel  7710  ixpexg  8860  rankuni  9778  unialeph  10014  ttukeylem1  10422  tgss2  22970  ordtbas2  23174  ordtbas  23175  ordttopon  23176  ordtopn1  23177  ordtopn2  23178  ordtrest2  23187  isref  23492  islocfin  23500  txbasex  23549  ptbasin2  23561  ordthmeolem  23784  alexsublem  24027  alexsub  24028  alexsubb  24029  ussid  24243  ordtrest2NEW  34107  brbigcup  36124  isfne  36567  isfne4  36568  isfne4b  36569  fnessref  36585  neibastop1  36587  fnejoin2  36597  prtex  39372