Theorem uniexg 7738

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 4887	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2854	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7737	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3531	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877

This theorem is referenced by:  uniex  7739  uniexd  7740  abnexg  7754  uniexb  7762  pwexr  7763  ssonuni  7778  ssonprc  7785  dmexg  7897  rnexg  7898  undefval  8272  onovuni  8328  tz7.44lem1  8391  tz7.44-3  8394  disjen  9121  domss2  9123  fival  9371  fipwuni  9385  supexd  9412  cantnflem1  9657  dfac8clem  10015  onssnum  10023  dfac12lem1  10126  dfac12lem2  10127  fin1a2lem12  10394  hsmexlem1  10409  wrdexb  14561  restid  17485  prdsbas  17509  prdsplusg  17510  prdsmulr  17511  prdsvsca  17512  prdshom  17519  sscpwex  17871  pmtrfv  19521  istopon  23037  tgval  23080  eltg2  23083  tgss2  23112  neiptoptop  23256  restin  23291  restntr  23307  cnprest2  23415  pnrmopn  23468  cnrmnrm  23486  cmpsublem  23524  cmpsub  23525  cmpcld  23527  hausmapdom  23625  isref  23634  locfindis  23655  txbasex  23691  dfac14lem  23742  xkopt  23780  xkopjcn  23781  qtopval2  23821  elqtop  23822  fbssfi  23962  ptcmplem2  24178  cnextfval  24187  tuslem  24391  madeval  27990  pliguhgr  30778  acunirnmpt2  32945  acunirnmpt2f  32946  ist0cld  34167  hasheuni  34419  insiga  34471  sigagenval  34474  omsval  34627  omssubadd  34634  sibfof  34674  sitmcl  34685  kur14  35606  cvmscld  35663  fobigcup  36288  hfuni  36574  isfne  36738  isfne4b  36740  fnemeet1  36765  tailfval  36771  bj-restuni2  37627  pibt2  37950  kelac2  43683  cnfex  45639  unidmex  45661  pwpwuni  45668  salgenval  46926  intsaluni  46934  salgenn0  46936  caragenunidm  47113  afv2ex  47839  iscnrm3rlem3  49604