Theorem uniexg 7726

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 4918	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7725	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3556	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  uniex  7727  uniexd  7728  abnexg  7739  uniexb  7747  pwexr  7748  ssonuni  7763  ssonprc  7771  dmexg  7890  rnexg  7891  undefval  8257  onovuni  8338  tz7.44lem1  8401  tz7.44-3  8404  en1unielOLD  9025  disjen  9130  domss2  9132  fival  9403  fipwuni  9417  supexd  9444  cantnflem1  9680  dfac8clem  10023  onssnum  10031  dfac12lem1  10134  dfac12lem2  10135  fin1a2lem12  10402  hsmexlem1  10417  wrdexb  14471  restid  17375  prdsbas  17399  prdsplusg  17400  prdsmulr  17401  prdsvsca  17402  prdshom  17409  sscpwex  17758  pmtrfv  19314  istopon  22405  tgval  22449  eltg2  22452  tgss2  22481  neiptoptop  22626  restin  22661  restntr  22677  cnprest2  22785  pnrmopn  22838  cnrmnrm  22856  cmpsublem  22894  cmpsub  22895  cmpcld  22897  hausmapdom  22995  isref  23004  locfindis  23025  txbasex  23061  dfac14lem  23112  xkopt  23150  xkopjcn  23151  qtopval2  23191  elqtop  23192  fbssfi  23332  ptcmplem2  23548  cnextfval  23557  tuslem  23762  tuslemOLD  23763  madeval  27336  pliguhgr  29726  acunirnmpt2  31872  acunirnmpt2f  31873  ist0cld  32801  hasheuni  33071  insiga  33123  sigagenval  33126  omsval  33280  omssubadd  33287  sibfof  33327  sitmcl  33338  kur14  34195  cvmscld  34252  fobigcup  34860  hfuni  35144  isfne  35212  isfne4b  35214  fnemeet1  35239  tailfval  35245  bj-restuni2  35967  pibt2  36286  imaexALTV  37187  kelac2  41792  cnfex  43697  unidmex  43722  pwpwuni  43729  salgenval  45023  intsaluni  45031  salgenn0  45033  caragenunidm  45210  afv2ex  45908  iscnrm3rlem3  47528