Theorem uniexg 7732

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 4919	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7731	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3556	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ∪ cuni 4908

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909

This theorem is referenced by:  uniex  7733  uniexd  7734  abnexg  7745  uniexb  7753  pwexr  7754  ssonuni  7769  ssonprc  7777  dmexg  7896  rnexg  7897  undefval  8263  onovuni  8344  tz7.44lem1  8407  tz7.44-3  8410  en1unielOLD  9031  disjen  9136  domss2  9138  fival  9409  fipwuni  9423  supexd  9450  cantnflem1  9686  dfac8clem  10029  onssnum  10037  dfac12lem1  10140  dfac12lem2  10141  fin1a2lem12  10408  hsmexlem1  10423  wrdexb  14479  restid  17383  prdsbas  17407  prdsplusg  17408  prdsmulr  17409  prdsvsca  17410  prdshom  17417  sscpwex  17766  pmtrfv  19361  istopon  22634  tgval  22678  eltg2  22681  tgss2  22710  neiptoptop  22855  restin  22890  restntr  22906  cnprest2  23014  pnrmopn  23067  cnrmnrm  23085  cmpsublem  23123  cmpsub  23124  cmpcld  23126  hausmapdom  23224  isref  23233  locfindis  23254  txbasex  23290  dfac14lem  23341  xkopt  23379  xkopjcn  23380  qtopval2  23420  elqtop  23421  fbssfi  23561  ptcmplem2  23777  cnextfval  23786  tuslem  23991  tuslemOLD  23992  madeval  27572  pliguhgr  29994  acunirnmpt2  32140  acunirnmpt2f  32141  ist0cld  33099  hasheuni  33369  insiga  33421  sigagenval  33424  omsval  33578  omssubadd  33585  sibfof  33625  sitmcl  33636  kur14  34493  cvmscld  34550  fobigcup  35164  hfuni  35448  isfne  35527  isfne4b  35529  fnemeet1  35554  tailfval  35560  bj-restuni2  36282  pibt2  36601  imaexALTV  37502  kelac2  42109  cnfex  44014  unidmex  44039  pwpwuni  44046  salgenval  45336  intsaluni  45344  salgenn0  45346  caragenunidm  45523  afv2ex  46221  iscnrm3rlem3  47663