Theorem uniexg 7316

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 4747	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2865	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7315	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3505	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079  Vcvv 3432  ∪ cuni 4739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088  ax-un 7310

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rex 3109  df-v 3434  df-uni 4740

This theorem is referenced by:  abnexg  7326  uniexb  7334  pwexr  7335  ssonuni  7348  ssonprc  7354  dmexg  7460  rnexg  7461  iunexg  7511  undefval  7784  onovuni  7822  tz7.44lem1  7884  tz7.44-3  7887  en1b  8415  en1uniel  8419  disjen  8511  domss2  8513  fival  8712  fipwuni  8726  supexd  8753  cantnflem1  8987  dfac8clem  9293  onssnum  9301  dfac12lem1  9404  dfac12lem2  9405  fin1a2lem12  9668  hsmexlem1  9683  axdc2lem  9705  ttukeylem3  9768  wrdexb  13707  restid  16524  prdsbas  16547  prdsplusg  16548  prdsmulr  16549  prdsvsca  16550  prdshom  16557  sscpwex  16902  pmtrfv  18299  frgpcyg  20390  istopon  21192  tgval  21235  eltg  21237  eltg2  21238  tgss2  21267  ntrval  21316  neiptoptop  21411  neiptopnei  21412  restin  21446  neitr  21460  restntr  21462  cnpresti  21568  cnprest  21569  cnprest2  21570  lmcnp  21584  pnrmopn  21623  cnrmnrm  21641  cmpsublem  21679  cmpsub  21680  cmpcld  21682  hausmapdom  21780  isref  21789  locfindis  21810  txbasex  21846  dfac14lem  21897  uptx  21905  xkopt  21935  xkopjcn  21936  qtopval2  21976  elqtop  21977  fbssfi  22117  ptcmplem2  22333  cnextfval  22342  cnextcn  22347  tuslem  22547  isppw  25361  pliguhgr  27942  elpwunicl  29975  acunirnmpt2  30068  acunirnmpt2f  30069  hasheuni  30917  insiga  30969  sigagenval  30972  braew  31074  omsval  31124  omssubaddlem  31130  omssubadd  31131  omsmeas  31154  sibfof  31171  sitmcl  31182  isrrvv  31274  rrvmulc  31284  bnj1489  31898  kur14  32027  cvmscld  32084  bdayimaon  32751  nosupno  32757  madeval  32843  fobigcup  32915  hfuni  33199  isfne  33241  isfne4b  33243  topjoin  33267  fnemeet1  33268  tailfval  33274  bj-restuni2  33934  pibt2  34175  mbfresfi  34415  supex2g  34490  imaexALTV  35068  kelac2  39101  cnfex  40776  unidmex  40803  pwpwuni  40810  uniexd  40859  unirnmap  40964  stoweidlem50  41831  stoweidlem57  41838  stoweidlem59  41840  stoweidlem60  41841  fourierdlem71  41958  salgenval  42102  intsaluni  42108  intsal  42109  salgenn0  42110  caragenval  42271  omecl  42281  caragenunidm  42286  afv2ex  42883  setrec1lem2  44225