Theorem uniexb 6973

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

Syntax hints:   ↔ wb 196   ∈ wcel 1990  Vcvv 3200  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437

This theorem is referenced by:  ixpexg  7932  rankuni  8726  unialeph  8924  ttukeylem1  9331  tgss2  20791  ordtbas2  20995  ordtbas  20996  ordttopon  20997  ordtopn1  20998  ordtopn2  20999  ordtrest2  21008  isref  21312  islocfin  21320  txbasex  21369  ptbasin2  21381  ordthmeolem  21604  alexsublem  21848  alexsub  21849  alexsubb  21850  ussid  22064  ordtrest2NEW  29969  omsfval  30356  brbigcup  32005  isfne  32334  isfne4  32335  isfne4b  32336  fnessref  32352  neibastop1  32354  fnejoin2  32364  prtex  34165