Theorem uniexb 7742

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253  ax-pow 5322  ax-un 7713

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3923  df-ss 3933  df-pw 4567  df-uni 4874

This theorem is referenced by:  elpwpwel  7745  ixpexg  8897  rankuni  9822  unialeph  10060  ttukeylem1  10468  tgss2  22880  ordtbas2  23084  ordtbas  23085  ordttopon  23086  ordtopn1  23087  ordtopn2  23088  ordtrest2  23097  isref  23402  islocfin  23410  txbasex  23459  ptbasin2  23471  ordthmeolem  23694  alexsublem  23937  alexsub  23938  alexsubb  23939  ussid  24154  ordtrest2NEW  33919  brbigcup  35881  isfne  36322  isfne4  36323  isfne4b  36324  fnessref  36340  neibastop1  36342  fnejoin2  36352  prtex  38868