Theorem uniexb 7778

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3451  ∪ cuni 4867

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-un 7751

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868

This theorem is used by:  elpwpwel  7781  ixpexg  8950  rankuni  9879  unialeph  10180  ttukeylem1  10587  tgss2  23305  ordtbas2  23509  ordtbas  23510  ordttopon  23511  ordtopn1  23512  ordtopn2  23513  ordtrest2  23522  isref  23828  islocfin  23836  txbasex  23885  ptbasin2  23897  ordthmeolem  24120  alexsublem  24363  alexsub  24364  alexsubb  24365  ussid  24579  ordtrest2NEW  34555  brbigcup  36660  isfne  37127  isfne4  37128  isfne4b  37129  fnessref  37145  neibastop1  37147  fnejoin2  37157  prtex  39937