Theorem uniexb 7759

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  Vcvv 3455  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564  df-uni 4873

This theorem is referenced by:  elpwpwel  7762  ixpexg  8916  rankuni  9831  unialeph  10081  ttukeylem1  10488  tgss2  23144  ordtbas2  23348  ordtbas  23349  ordttopon  23350  ordtopn1  23351  ordtopn2  23352  ordtrest2  23361  isref  23666  islocfin  23674  txbasex  23723  ptbasin2  23735  ordthmeolem  23958  alexsublem  24201  alexsub  24202  alexsubb  24203  ussid  24417  ordtrest2NEW  34313  brbigcup  36388  isfne  36870  isfne4  36871  isfne4b  36872  fnessref  36888  neibastop1  36890  fnejoin2  36900  prtex  39674