Theorem uniexg 4361

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 3745	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2208	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vex 2689	. . 3 ⊢ 𝑥 ∈ V
4	3	uniex 4359	. 2 ⊢ ∪ 𝑥 ∈ V
5	2, 4	vtoclg 2746	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  Vcvv 2686  ∪ cuni 3736

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-un 4355

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-uni 3737

This theorem is referenced by:  abnexg  4367  snnex  4369  uniexb  4394  ssonuni  4404  dmexg  4803  rnexg  4804  elxp4  5026  elxp5  5027  relrnfvex  5439  fvexg  5440  sefvex  5442  riotaexg  5734  iunexg  6017  1stvalg  6040  2ndvalg  6041  cnvf1o  6122  brtpos2  6148  tfrlemiex  6228  tfr1onlemex  6244  tfrcllemex  6257  en1bg  6694  en1uniel  6698  fival  6858  suplocexprlem2b  7522  suplocexprlemlub  7532  restid  12131  istopon  12180  tgval  12218  tgvalex  12219  eltg  12221  eltg2  12222  tgss2  12248  ntrval  12279  restin  12345  cnovex  12365  cnprcl2k  12375  cnptopresti  12407  cnptoprest  12408  cnptoprest2  12409  lmtopcnp  12419  txbasex  12426  uptx  12443  reldvg  12817