Theorem uniexg 4441

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 3820	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2246	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vex 2742	. . 3 ⊢ 𝑥 ∈ V
4	3	uniex 4439	. 2 ⊢ ∪ 𝑥 ∈ V
5	2, 4	vtoclg 2799	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  Vcvv 2739  ∪ cuni 3811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-un 4435

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-uni 3812

This theorem is referenced by:  uniexd  4442  abnexg  4448  snnex  4450  uniexb  4475  ssonuni  4489  dmexg  4893  rnexg  4894  elxp4  5118  elxp5  5119  relrnfvex  5535  fvexg  5536  sefvex  5538  riotaexg  5838  iunexg  6123  1stvalg  6146  2ndvalg  6147  cnvf1o  6229  brtpos2  6255  tfrlemiex  6335  tfr1onlemex  6351  tfrcllemex  6364  en1bg  6803  en1uniel  6807  fival  6972  suplocexprlem2b  7716  suplocexprlemlub  7726  restid  12705  tgval  12717  tgvalex  12718  istopon  13701  eltg  13740  eltg2  13741  tgss2  13767  ntrval  13798  restin  13864  cnovex  13884  cnprcl2k  13894  cnptopresti  13926  cnptoprest  13927  cnptoprest2  13928  lmtopcnp  13938  txbasex  13945  uptx  13962  reldvg  14336