Theorem uniexb 7697

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pow 5301  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549  df-uni 4857

This theorem is referenced by:  elpwpwel  7700  ixpexg  8846  rankuni  9756  unialeph  9992  ttukeylem1  10400  tgss2  22902  ordtbas2  23106  ordtbas  23107  ordttopon  23108  ordtopn1  23109  ordtopn2  23110  ordtrest2  23119  isref  23424  islocfin  23432  txbasex  23481  ptbasin2  23493  ordthmeolem  23716  alexsublem  23959  alexsub  23960  alexsubb  23961  ussid  24175  ordtrest2NEW  33936  brbigcup  35940  isfne  36383  isfne4  36384  isfne4b  36385  fnessref  36401  neibastop1  36403  fnejoin2  36413  prtex  38989