Theorem uniexb 7720

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

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 2701  ax-sep 5246  ax-pow 5315  ax-un 7691

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561  df-uni 4868

This theorem is referenced by:  elpwpwel  7723  ixpexg  8872  rankuni  9792  unialeph  10030  ttukeylem1  10438  tgss2  22907  ordtbas2  23111  ordtbas  23112  ordttopon  23113  ordtopn1  23114  ordtopn2  23115  ordtrest2  23124  isref  23429  islocfin  23437  txbasex  23486  ptbasin2  23498  ordthmeolem  23721  alexsublem  23964  alexsub  23965  alexsubb  23966  ussid  24181  ordtrest2NEW  33906  brbigcup  35879  isfne  36320  isfne4  36321  isfne4b  36322  fnessref  36338  neibastop1  36340  fnejoin2  36350  prtex  38866