Theorem uniexg 7760

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 2826	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7759	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3554	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∪ cuni 4907

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 2708  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  uniex  7761  uniexd  7762  abnexg  7776  uniexb  7784  pwexr  7785  ssonuni  7800  ssonprc  7807  dmexg  7923  rnexg  7924  undefval  8301  onovuni  8382  tz7.44lem1  8445  tz7.44-3  8448  disjen  9174  domss2  9176  fival  9452  fipwuni  9466  supexd  9493  cantnflem1  9729  dfac8clem  10072  onssnum  10080  dfac12lem1  10184  dfac12lem2  10185  fin1a2lem12  10451  hsmexlem1  10466  wrdexb  14563  restid  17478  prdsbas  17502  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  sscpwex  17859  pmtrfv  19470  istopon  22918  tgval  22962  eltg2  22965  tgss2  22994  neiptoptop  23139  restin  23174  restntr  23190  cnprest2  23298  pnrmopn  23351  cnrmnrm  23369  cmpsublem  23407  cmpsub  23408  cmpcld  23410  hausmapdom  23508  isref  23517  locfindis  23538  txbasex  23574  dfac14lem  23625  xkopt  23663  xkopjcn  23664  qtopval2  23704  elqtop  23705  fbssfi  23845  ptcmplem2  24061  cnextfval  24070  tuslem  24275  tuslemOLD  24276  madeval  27891  pliguhgr  30505  acunirnmpt2  32670  acunirnmpt2f  32671  ist0cld  33832  hasheuni  34086  insiga  34138  sigagenval  34141  omsval  34295  omssubadd  34302  sibfof  34342  sitmcl  34353  kur14  35221  cvmscld  35278  fobigcup  35901  hfuni  36185  isfne  36340  isfne4b  36342  fnemeet1  36367  tailfval  36373  bj-restuni2  37099  pibt2  37418  imaexALTV  38331  kelac2  43077  cnfex  45033  unidmex  45055  pwpwuni  45062  salgenval  46336  intsaluni  46344  salgenn0  46346  caragenunidm  46523  afv2ex  47226  iscnrm3rlem3  48839