Theorem uniexb 7719

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558  df-uni 4866

This theorem is referenced by:  elpwpwel  7722  ixpexg  8872  rankuni  9787  unialeph  10023  ttukeylem1  10431  tgss2  22943  ordtbas2  23147  ordtbas  23148  ordttopon  23149  ordtopn1  23150  ordtopn2  23151  ordtrest2  23160  isref  23465  islocfin  23473  txbasex  23522  ptbasin2  23534  ordthmeolem  23757  alexsublem  24000  alexsub  24001  alexsubb  24002  ussid  24216  ordtrest2NEW  34101  brbigcup  36112  isfne  36555  isfne4  36556  isfne4b  36557  fnessref  36573  neibastop1  36575  fnejoin2  36585  prtex  39256