Theorem uniexg 7734

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 4894	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7733	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3533	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  uniex  7735  uniexd  7736  abnexg  7750  uniexb  7758  pwexr  7759  ssonuni  7774  ssonprc  7781  dmexg  7897  rnexg  7898  undefval  8275  onovuni  8356  tz7.44lem1  8419  tz7.44-3  8422  disjen  9148  domss2  9150  fival  9424  fipwuni  9438  supexd  9465  cantnflem1  9703  dfac8clem  10046  onssnum  10054  dfac12lem1  10158  dfac12lem2  10159  fin1a2lem12  10425  hsmexlem1  10440  wrdexb  14543  restid  17447  prdsbas  17471  prdsplusg  17472  prdsmulr  17473  prdsvsca  17474  prdshom  17481  sscpwex  17828  pmtrfv  19433  istopon  22850  tgval  22893  eltg2  22896  tgss2  22925  neiptoptop  23069  restin  23104  restntr  23120  cnprest2  23228  pnrmopn  23281  cnrmnrm  23299  cmpsublem  23337  cmpsub  23338  cmpcld  23340  hausmapdom  23438  isref  23447  locfindis  23468  txbasex  23504  dfac14lem  23555  xkopt  23593  xkopjcn  23594  qtopval2  23634  elqtop  23635  fbssfi  23775  ptcmplem2  23991  cnextfval  24000  tuslem  24205  madeval  27812  pliguhgr  30467  acunirnmpt2  32638  acunirnmpt2f  32639  ist0cld  33864  hasheuni  34116  insiga  34168  sigagenval  34171  omsval  34325  omssubadd  34332  sibfof  34372  sitmcl  34383  kur14  35238  cvmscld  35295  fobigcup  35918  hfuni  36202  isfne  36357  isfne4b  36359  fnemeet1  36384  tailfval  36390  bj-restuni2  37116  pibt2  37435  imaexALTV  38348  kelac2  43089  cnfex  45052  unidmex  45074  pwpwuni  45081  salgenval  46350  intsaluni  46358  salgenn0  46360  caragenunidm  46537  afv2ex  47243  iscnrm3rlem3  48916