Theorem uniexg 4416

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 3797	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2234	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vex 2728	. . 3 ⊢ 𝑥 ∈ V
4	3	uniex 4414	. 2 ⊢ ∪ 𝑥 ∈ V
5	2, 4	vtoclg 2785	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  Vcvv 2725  ∪ cuni 3788

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-un 4410

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-uni 3789

This theorem is referenced by:  uniexd  4417  abnexg  4423  snnex  4425  uniexb  4450  ssonuni  4464  dmexg  4867  rnexg  4868  elxp4  5090  elxp5  5091  relrnfvex  5503  fvexg  5504  sefvex  5506  riotaexg  5801  iunexg  6084  1stvalg  6107  2ndvalg  6108  cnvf1o  6189  brtpos2  6215  tfrlemiex  6295  tfr1onlemex  6311  tfrcllemex  6324  en1bg  6762  en1uniel  6766  fival  6931  suplocexprlem2b  7651  suplocexprlemlub  7661  restid  12562  istopon  12611  tgval  12649  tgvalex  12650  eltg  12652  eltg2  12653  tgss2  12679  ntrval  12710  restin  12776  cnovex  12796  cnprcl2k  12806  cnptopresti  12838  cnptoprest  12839  cnptoprest2  12840  lmtopcnp  12850  txbasex  12857  uptx  12874  reldvg  13248