Theorem uniexb 7634

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

Syntax hints:   ↔ wb 205   ∈ wcel 2101  Vcvv 3434  ∪ cuni 4841

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 2103  ax-9 2111  ax-ext 2704  ax-sep 5226  ax-pow 5291  ax-un 7608

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3224  df-v 3436  df-in 3896  df-ss 3906  df-pw 4538  df-uni 4842

This theorem is referenced by:  elpwpwel  7637  ixpexg  8730  rankuni  9649  unialeph  9885  ttukeylem1  10293  tgss2  22165  ordtbas2  22370  ordtbas  22371  ordttopon  22372  ordtopn1  22373  ordtopn2  22374  ordtrest2  22383  isref  22688  islocfin  22696  txbasex  22745  ptbasin2  22757  ordthmeolem  22980  alexsublem  23223  alexsub  23224  alexsubb  23225  ussid  23440  ordtrest2NEW  31901  brbigcup  34228  isfne  34556  isfne4  34557  isfne4b  34558  fnessref  34574  neibastop1  34576  fnejoin2  34586  prtex  36920