Theorem uniexb 7799

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624  df-uni 4932

This theorem is referenced by:  elpwpwel  7802  ixpexg  8980  rankuni  9932  unialeph  10170  ttukeylem1  10578  tgss2  23015  ordtbas2  23220  ordtbas  23221  ordttopon  23222  ordtopn1  23223  ordtopn2  23224  ordtrest2  23233  isref  23538  islocfin  23546  txbasex  23595  ptbasin2  23607  ordthmeolem  23830  alexsublem  24073  alexsub  24074  alexsubb  24075  ussid  24290  ordtrest2NEW  33869  brbigcup  35862  isfne  36305  isfne4  36306  isfne4b  36307  fnessref  36323  neibastop1  36325  fnejoin2  36335  prtex  38836