Theorem uniexg 7673

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 4867	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2816	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7672	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3507	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  uniex  7674  uniexd  7675  abnexg  7689  uniexb  7697  pwexr  7698  ssonuni  7713  ssonprc  7720  dmexg  7831  rnexg  7832  undefval  8206  onovuni  8262  tz7.44lem1  8324  tz7.44-3  8327  disjen  9047  domss2  9049  fival  9296  fipwuni  9310  supexd  9337  cantnflem1  9579  dfac8clem  9923  onssnum  9931  dfac12lem1  10035  dfac12lem2  10036  fin1a2lem12  10302  hsmexlem1  10317  wrdexb  14432  restid  17337  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  sscpwex  17722  pmtrfv  19364  istopon  22827  tgval  22870  eltg2  22873  tgss2  22902  neiptoptop  23046  restin  23081  restntr  23097  cnprest2  23205  pnrmopn  23258  cnrmnrm  23276  cmpsublem  23314  cmpsub  23315  cmpcld  23317  hausmapdom  23415  isref  23424  locfindis  23445  txbasex  23481  dfac14lem  23532  xkopt  23570  xkopjcn  23571  qtopval2  23611  elqtop  23612  fbssfi  23752  ptcmplem2  23968  cnextfval  23977  tuslem  24181  madeval  27793  pliguhgr  30466  acunirnmpt2  32642  acunirnmpt2f  32643  ist0cld  33846  hasheuni  34098  insiga  34150  sigagenval  34153  omsval  34306  omssubadd  34313  sibfof  34353  sitmcl  34364  kur14  35260  cvmscld  35317  fobigcup  35942  hfuni  36228  isfne  36383  isfne4b  36385  fnemeet1  36410  tailfval  36416  bj-restuni2  37142  pibt2  37461  kelac2  43157  cnfex  45124  unidmex  45146  pwpwuni  45153  salgenval  46418  intsaluni  46426  salgenn0  46428  caragenunidm  46605  afv2ex  47313  iscnrm3rlem3  49041