Theorem uniexb 7747

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3474  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-pow 5362  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-pw 4603  df-uni 4908

This theorem is referenced by:  elpwpwel  7750  ixpexg  8912  rankuni  9854  unialeph  10092  ttukeylem1  10500  tgss2  22481  ordtbas2  22686  ordtbas  22687  ordttopon  22688  ordtopn1  22689  ordtopn2  22690  ordtrest2  22699  isref  23004  islocfin  23012  txbasex  23061  ptbasin2  23073  ordthmeolem  23296  alexsublem  23539  alexsub  23540  alexsubb  23541  ussid  23756  ordtrest2NEW  32891  brbigcup  34858  isfne  35212  isfne4  35213  isfne4b  35214  fnessref  35230  neibastop1  35232  fnejoin2  35242  prtex  37738