Theorem uniexb 7764

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3450  ∪ 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 2732  ax-sep 5251  ax-pow 5330  ax-un 7737

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868

This theorem is used by:  elpwpwel  7767  ixpexg  8932  rankuni  9848  unialeph  10107  ttukeylem1  10514  tgss2  23215  ordtbas2  23419  ordtbas  23420  ordttopon  23421  ordtopn1  23422  ordtopn2  23423  ordtrest2  23432  isref  23738  islocfin  23746  txbasex  23795  ptbasin2  23807  ordthmeolem  24030  alexsublem  24273  alexsub  24274  alexsubb  24275  ussid  24489  ordtrest2NEW  34436  brbigcup  36478  isfne  36961  isfne4  36962  isfne4b  36963  fnessref  36979  neibastop1  36981  fnejoin2  36991  prtex  39756