Theorem uniexb 7763

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3464  ∪ cuni 4888

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 2708  ax-sep 5271  ax-pow 5340  ax-un 7734

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-in 3938  df-ss 3948  df-pw 4582  df-uni 4889

This theorem is referenced by:  elpwpwel  7766  ixpexg  8941  rankuni  9882  unialeph  10120  ttukeylem1  10528  tgss2  22930  ordtbas2  23134  ordtbas  23135  ordttopon  23136  ordtopn1  23137  ordtopn2  23138  ordtrest2  23147  isref  23452  islocfin  23460  txbasex  23509  ptbasin2  23521  ordthmeolem  23744  alexsublem  23987  alexsub  23988  alexsubb  23989  ussid  24204  ordtrest2NEW  33959  brbigcup  35921  isfne  36362  isfne4  36363  isfne4b  36364  fnessref  36380  neibastop1  36382  fnejoin2  36392  prtex  38903