Theorem uniexb 7488

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Vcvv 3496  ∪ cuni 4840

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-pow 5268  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543  df-uni 4841

This theorem is referenced by:  elpwpwel  7491  ixpexg  8488  rankuni  9294  unialeph  9529  ttukeylem1  9933  tgss2  21597  ordtbas2  21801  ordtbas  21802  ordttopon  21803  ordtopn1  21804  ordtopn2  21805  ordtrest2  21814  isref  22119  islocfin  22127  txbasex  22176  ptbasin2  22188  ordthmeolem  22411  alexsublem  22654  alexsub  22655  alexsubb  22656  ussid  22871  ordtrest2NEW  31168  brbigcup  33361  isfne  33689  isfne4  33690  isfne4b  33691  fnessref  33707  neibastop1  33709  fnejoin2  33719  prtex  36018