Theorem uniexb 6866

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 6853	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
2		pwuni 4825	. . 3 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
3		pwexg 4776	. . 3 ⊢ (∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ∈ V)
4		ssexg 4732	. . 3 ⊢ ((𝐴 ⊆ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ∈ V) → 𝐴 ∈ V)
5	2, 3, 4	sylancr 694	. 2 ⊢ (∪ 𝐴 ∈ V → 𝐴 ∈ V)
6	1, 5	impbii 198	1 ⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)

Syntax hints:   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373

This theorem is referenced by:  pwexb  6867  ssonprc  6884  ixpexg  7818  rankuni  8609  ac5num  8742  unialeph  8807  ttukeylem1  9214  tgss2  20602  ordtbas2  20805  ordtbas  20806  ordttopon  20807  ordtopn1  20808  ordtopn2  20809  ordtrest2  20818  isref  21122  islocfin  21130  txbasex  21179  ptbasin2  21191  ordthmeolem  21414  alexsublem  21658  alexsub  21659  alexsubb  21660  ussid  21874  ordtrest2NEW  29297  omsfval  29683  brbigcup  31175  isfne  31504  isfne4  31505  isfne4b  31506  fnessref  31522  neibastop1  31524  fnejoin2  31534  bj-restv  32229  prtex  33183