Theorem uniexg 7683

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 4851	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2820	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7682	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3497	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3427  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-ss 3902  df-uni 4841

This theorem is referenced by:  uniex  7684  uniexd  7685  abnexg  7699  uniexb  7707  pwexr  7708  ssonuni  7723  ssonprc  7730  dmexg  7841  rnexg  7842  undefval  8215  onovuni  8271  tz7.44lem1  8333  tz7.44-3  8336  disjen  9061  domss2  9063  fival  9314  fipwuni  9328  supexd  9355  cantnflem1  9599  dfac8clem  9943  onssnum  9951  dfac12lem1  10055  dfac12lem2  10056  fin1a2lem12  10322  hsmexlem1  10337  wrdexb  14476  restid  17385  prdsbas  17409  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdshom  17419  sscpwex  17771  pmtrfv  19416  istopon  22865  tgval  22908  eltg2  22911  tgss2  22940  neiptoptop  23084  restin  23119  restntr  23135  cnprest2  23243  pnrmopn  23296  cnrmnrm  23314  cmpsublem  23352  cmpsub  23353  cmpcld  23355  hausmapdom  23453  isref  23462  locfindis  23483  txbasex  23519  dfac14lem  23570  xkopt  23608  xkopjcn  23609  qtopval2  23649  elqtop  23650  fbssfi  23790  ptcmplem2  24006  cnextfval  24015  tuslem  24219  madeval  27812  pliguhgr  30545  acunirnmpt2  32721  acunirnmpt2f  32722  ist0cld  33965  hasheuni  34217  insiga  34269  sigagenval  34272  omsval  34425  omssubadd  34432  sibfof  34472  sitmcl  34483  kur14  35386  cvmscld  35443  fobigcup  36068  hfuni  36354  isfne  36509  isfne4b  36511  fnemeet1  36536  tailfval  36542  bj-restuni2  37398  pibt2  37721  kelac2  43481  cnfex  45447  unidmex  45469  pwpwuni  45476  salgenval  46737  intsaluni  46745  salgenn0  46747  caragenunidm  46924  afv2ex  47650  iscnrm3rlem3  49405