Theorem uniexb 7709

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3440  ∪ cuni 4863

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556  df-uni 4864

This theorem is referenced by:  elpwpwel  7712  ixpexg  8860  rankuni  9775  unialeph  10011  ttukeylem1  10419  tgss2  22931  ordtbas2  23135  ordtbas  23136  ordttopon  23137  ordtopn1  23138  ordtopn2  23139  ordtrest2  23148  isref  23453  islocfin  23461  txbasex  23510  ptbasin2  23522  ordthmeolem  23745  alexsublem  23988  alexsub  23989  alexsubb  23990  ussid  24204  ordtrest2NEW  34080  brbigcup  36090  isfne  36533  isfne4  36534  isfne4b  36535  fnessref  36551  neibastop1  36553  fnejoin2  36563  prtex  39150