Theorem uniexb 7466

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

Syntax hints:   ↔ wb 209   ∈ wcel 2111  Vcvv 3441  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499  df-uni 4801

This theorem is referenced by:  elpwpwel  7469  ixpexg  8469  rankuni  9276  unialeph  9512  ttukeylem1  9920  tgss2  21592  ordtbas2  21796  ordtbas  21797  ordttopon  21798  ordtopn1  21799  ordtopn2  21800  ordtrest2  21809  isref  22114  islocfin  22122  txbasex  22171  ptbasin2  22183  ordthmeolem  22406  alexsublem  22649  alexsub  22650  alexsubb  22651  ussid  22866  ordtrest2NEW  31276  brbigcup  33472  isfne  33800  isfne4  33801  isfne4b  33802  fnessref  33818  neibastop1  33820  fnejoin2  33830  prtex  36176