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  5837  iunexg  6122  1stvalg  6145  2ndvalg  6146  cnvf1o  6228  brtpos2  6254  tfrlemiex  6334  tfr1onlemex  6350  tfrcllemex  6363  en1bg  6802  en1uniel  6806  fival  6971  suplocexprlem2b  7715  suplocexprlemlub  7725  restid  12704  tgval  12716  tgvalex  12717  istopon  13552  eltg  13591  eltg2  13592  tgss2  13618  ntrval  13649  restin  13715  cnovex  13735  cnprcl2k  13745  cnptopresti  13777  cnptoprest  13778  cnptoprest2  13779  lmtopcnp  13789  txbasex  13796  uptx  13813  reldvg  14187