Theorem uniexb 7740

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pow 5320  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565  df-uni 4872

This theorem is referenced by:  elpwpwel  7743  ixpexg  8895  rankuni  9816  unialeph  10054  ttukeylem1  10462  tgss2  22874  ordtbas2  23078  ordtbas  23079  ordttopon  23080  ordtopn1  23081  ordtopn2  23082  ordtrest2  23091  isref  23396  islocfin  23404  txbasex  23453  ptbasin2  23465  ordthmeolem  23688  alexsublem  23931  alexsub  23932  alexsubb  23933  ussid  24148  ordtrest2NEW  33913  brbigcup  35886  isfne  36327  isfne4  36328  isfne4b  36329  fnessref  36345  neibastop1  36347  fnejoin2  36357  prtex  38873