Theorem uniexg 4424

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.)

Assertion

Ref	Expression
uniexg	⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Proof of Theorem uniexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 3805	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2239	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vex 2733	. . 3 ⊢ 𝑥 ∈ V
4	3	uniex 4422	. 2 ⊢ ∪ 𝑥 ∈ V
5	2, 4	vtoclg 2790	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  Vcvv 2730  ∪ cuni 3796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-un 4418

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-uni 3797

This theorem is referenced by:  uniexd  4425  abnexg  4431  snnex  4433  uniexb  4458  ssonuni  4472  dmexg  4875  rnexg  4876  elxp4  5098  elxp5  5099  relrnfvex  5514  fvexg  5515  sefvex  5517  riotaexg  5813  iunexg  6098  1stvalg  6121  2ndvalg  6122  cnvf1o  6204  brtpos2  6230  tfrlemiex  6310  tfr1onlemex  6326  tfrcllemex  6339  en1bg  6778  en1uniel  6782  fival  6947  suplocexprlem2b  7676  suplocexprlemlub  7686  restid  12590  istopon  12805  tgval  12843  tgvalex  12844  eltg  12846  eltg2  12847  tgss2  12873  ntrval  12904  restin  12970  cnovex  12990  cnprcl2k  13000  cnptopresti  13032  cnptoprest  13033  cnptoprest2  13034  lmtopcnp  13044  txbasex  13051  uptx  13068  reldvg  13442