Theorem uniexb 7238

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

Syntax hints:   ↔ wb 198   ∈ wcel 2164  Vcvv 3414  ∪ cuni 4660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803  ax-sep 5007  ax-pow 5067  ax-un 7214

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-v 3416  df-in 3805  df-ss 3812  df-pw 4382  df-uni 4661

This theorem is referenced by:  elpwpwel  7241  ixpexg  8205  rankuni  9010  unialeph  9244  ttukeylem1  9653  tgss2  21169  ordtbas2  21373  ordtbas  21374  ordttopon  21375  ordtopn1  21376  ordtopn2  21377  ordtrest2  21386  isref  21690  islocfin  21698  txbasex  21747  ptbasin2  21759  ordthmeolem  21982  alexsublem  22225  alexsub  22226  alexsubb  22227  ussid  22441  ordtrest2NEW  30510  omsfval  30897  brbigcup  32539  isfne  32867  isfne4  32868  isfne4b  32869  fnessref  32885  neibastop1  32887  fnejoin2  32897  prtex  34950