Theorem uniexb 7592

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532  df-uni 4837

This theorem is referenced by:  elpwpwel  7595  ixpexg  8668  rankuni  9552  unialeph  9788  ttukeylem1  10196  tgss2  22045  ordtbas2  22250  ordtbas  22251  ordttopon  22252  ordtopn1  22253  ordtopn2  22254  ordtrest2  22263  isref  22568  islocfin  22576  txbasex  22625  ptbasin2  22637  ordthmeolem  22860  alexsublem  23103  alexsub  23104  alexsubb  23105  ussid  23320  ordtrest2NEW  31775  brbigcup  34127  isfne  34455  isfne4  34456  isfne4b  34457  fnessref  34473  neibastop1  34475  fnejoin2  34485  prtex  36821