Theorem uniexb 7485

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

Syntax hints:   ↔ wb 208   ∈ wcel 2110  Vcvv 3494  ∪ cuni 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-pow 5265  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951  df-pw 4540  df-uni 4838

This theorem is referenced by:  elpwpwel  7488  ixpexg  8485  rankuni  9291  unialeph  9526  ttukeylem1  9930  tgss2  21594  ordtbas2  21798  ordtbas  21799  ordttopon  21800  ordtopn1  21801  ordtopn2  21802  ordtrest2  21811  isref  22116  islocfin  22124  txbasex  22173  ptbasin2  22185  ordthmeolem  22408  alexsublem  22651  alexsub  22652  alexsubb  22653  ussid  22868  ordtrest2NEW  31166  brbigcup  33359  isfne  33687  isfne4  33688  isfne4b  33689  fnessref  33705  neibastop1  33707  fnejoin2  33717  prtex  36015