Theorem uniexb 7785

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  Vcvv 3453  ∪ cuni 4869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pow 5330  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-in 4093  df-pw 4561  df-uni 4870

This theorem is used by:  elpwpwel  7788  ixpexg  8961  rankuni  9889  unialeph  10190  ttukeylem1  10597  tgss2  23317  ordtbas2  23521  ordtbas  23522  ordttopon  23523  ordtopn1  23524  ordtopn2  23525  ordtrest2  23534  isref  23840  islocfin  23848  txbasex  23897  ptbasin2  23909  ordthmeolem  24132  alexsublem  24375  alexsub  24376  alexsubb  24377  ussid  24591  ordtrest2NEW  34608  brbigcup  36787  isfne  37254  isfne4  37255  isfne4b  37256  fnessref  37272  neibastop1  37274  fnejoin2  37284  prtex  40077