Theorem uniexb 7783

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

Syntax hints:   ↔ wb 206   ∈ wcel 2106  Vcvv 3478  ∪ cuni 4912

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pow 5371  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-pw 4607  df-uni 4913

This theorem is referenced by:  elpwpwel  7786  ixpexg  8961  rankuni  9901  unialeph  10139  ttukeylem1  10547  tgss2  23010  ordtbas2  23215  ordtbas  23216  ordttopon  23217  ordtopn1  23218  ordtopn2  23219  ordtrest2  23228  isref  23533  islocfin  23541  txbasex  23590  ptbasin2  23602  ordthmeolem  23825  alexsublem  24068  alexsub  24069  alexsubb  24070  ussid  24285  ordtrest2NEW  33884  brbigcup  35880  isfne  36322  isfne4  36323  isfne4b  36324  fnessref  36340  neibastop1  36342  fnejoin2  36352  prtex  38862