Theorem uniexb 7769

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566  df-uni 4875

This theorem is used by:  elpwpwel  7772  ixpexg  8926  rankuni  9842  unialeph  10101  ttukeylem1  10508  tgss2  23196  ordtbas2  23400  ordtbas  23401  ordttopon  23402  ordtopn1  23403  ordtopn2  23404  ordtrest2  23413  isref  23719  islocfin  23727  txbasex  23776  ptbasin2  23788  ordthmeolem  24011  alexsublem  24254  alexsub  24255  alexsubb  24256  ussid  24470  ordtrest2NEW  34379  brbigcup  36427  isfne  36909  isfne4  36910  isfne4b  36911  fnessref  36927  neibastop1  36929  fnejoin2  36939  prtex  39714