Theorem uniexg 7725

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 4878	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2849	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7724	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3524	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144  Vcvv 3456  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868

This theorem is referenced by:  uniex  7726  uniexd  7727  abnexg  7741  uniexb  7749  pwexr  7750  ssonuni  7765  ssonprc  7772  dmexg  7884  rnexg  7885  undefval  8259  onovuni  8315  tz7.44lem1  8378  tz7.44-3  8381  disjen  9108  domss2  9110  fival  9360  fipwuni  9374  supexd  9401  cantnflem1  9646  dfac8clem  9990  onssnum  9998  dfac12lem1  10102  dfac12lem2  10103  fin1a2lem12  10370  hsmexlem1  10385  wrdexb  14540  restid  17464  prdsbas  17488  prdsplusg  17489  prdsmulr  17490  prdsvsca  17491  prdshom  17498  sscpwex  17850  pmtrfv  19494  istopon  22974  tgval  23017  eltg2  23020  tgss2  23049  neiptoptop  23193  restin  23228  restntr  23244  cnprest2  23352  pnrmopn  23405  cnrmnrm  23423  cmpsublem  23461  cmpsub  23462  cmpcld  23464  hausmapdom  23562  isref  23571  locfindis  23592  txbasex  23628  dfac14lem  23679  xkopt  23717  xkopjcn  23718  qtopval2  23758  elqtop  23759  fbssfi  23899  ptcmplem2  24115  cnextfval  24124  tuslem  24328  madeval  27927  pliguhgr  30691  acunirnmpt2  32864  acunirnmpt2f  32865  ist0cld  34132  hasheuni  34384  insiga  34436  sigagenval  34439  omsval  34592  omssubadd  34599  sibfof  34639  sitmcl  34650  kur14  35571  cvmscld  35628  fobigcup  36253  hfuni  36539  isfne  36704  isfne4b  36706  fnemeet1  36731  tailfval  36737  bj-restuni2  37593  pibt2  37916  kelac2  43647  cnfex  45613  unidmex  45635  pwpwuni  45642  salgenval  46900  intsaluni  46908  salgenn0  46910  caragenunidm  47087  afv2ex  47813  iscnrm3rlem3  49568