Theorem uniexg 7759

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  Vcvv 3478  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913

This theorem is referenced by:  uniex  7760  uniexd  7761  abnexg  7775  uniexb  7783  pwexr  7784  ssonuni  7799  ssonprc  7807  dmexg  7924  rnexg  7925  undefval  8300  onovuni  8381  tz7.44lem1  8444  tz7.44-3  8447  disjen  9173  domss2  9175  fival  9450  fipwuni  9464  supexd  9491  cantnflem1  9727  dfac8clem  10070  onssnum  10078  dfac12lem1  10182  dfac12lem2  10183  fin1a2lem12  10449  hsmexlem1  10464  wrdexb  14560  restid  17480  prdsbas  17504  prdsplusg  17505  prdsmulr  17506  prdsvsca  17507  prdshom  17514  sscpwex  17863  pmtrfv  19485  istopon  22934  tgval  22978  eltg2  22981  tgss2  23010  neiptoptop  23155  restin  23190  restntr  23206  cnprest2  23314  pnrmopn  23367  cnrmnrm  23385  cmpsublem  23423  cmpsub  23424  cmpcld  23426  hausmapdom  23524  isref  23533  locfindis  23554  txbasex  23590  dfac14lem  23641  xkopt  23679  xkopjcn  23680  qtopval2  23720  elqtop  23721  fbssfi  23861  ptcmplem2  24077  cnextfval  24086  tuslem  24291  tuslemOLD  24292  madeval  27906  pliguhgr  30515  acunirnmpt2  32677  acunirnmpt2f  32678  ist0cld  33794  hasheuni  34066  insiga  34118  sigagenval  34121  omsval  34275  omssubadd  34282  sibfof  34322  sitmcl  34333  kur14  35201  cvmscld  35258  fobigcup  35882  hfuni  36166  isfne  36322  isfne4b  36324  fnemeet1  36349  tailfval  36355  bj-restuni2  37081  pibt2  37400  imaexALTV  38312  kelac2  43054  cnfex  44966  unidmex  44990  pwpwuni  44997  salgenval  46277  intsaluni  46285  salgenn0  46287  caragenunidm  46464  afv2ex  47164  iscnrm3rlem3  48739