Theorem uniexd 7689

Description: Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
uniexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
uniexd	⊢ (𝜑 → ∪ 𝐴 ∈ V)

Proof of Theorem uniexd

Step	Hyp	Ref	Expression
1		uniexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		uniexg 7687	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433  ∪ cuni 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842

This theorem is referenced by:  unexg  7690  iunexg  7909  cofon1  8602  cofon2  8603  axdc2lem  10365  ttukeylem3  10428  ghmqusnsglem1  19250  ghmqusnsg  19252  ghmquskerlem1  19253  ghmquskerco  19254  ghmquskerlem3  19256  ghmqusker  19257  frgpcyg  21552  eltg  22944  ntrval  23023  neiptopnei  23119  neitr  23167  cnpresti  23275  cnprest  23276  lmcnp  23291  uptx  23612  cnextcn  24054  isppw  27099  bdayimaon  27679  nosupno  27689  noinfno  27704  noeta2  27775  etaslts2  27808  cutbdaybnd2lim  27811  oldval  27848  elrspunidl  33515  algextdeglem4  33916  braew  34438  omsfval  34490  omssubaddlem  34495  omssubadd  34496  omsmeas  34519  sibfof  34536  isrrvv  34639  rrvmulc  34649  bnj1489  35253  isfne4  36583  topjoin  36608  mbfresfi  38048  supex2g  38119  restuni4  45582  unirnmap  45667  stoweidlem50  46507  stoweidlem57  46514  stoweidlem59  46516  stoweidlem60  46517  fourierdlem71  46634  intsal  46787  subsaluni  46817  caragenval  46950  omecl  46960  issmflem  47184  issmflelem  47201  issmfle  47202  smfconst  47206  issmfgtlem  47212  issmfgt  47213  issmfgelem  47226  issmfge  47227  smfpimioo  47244  smfresal  47245  fundcmpsurinjlem3  47889  iscnrm3rlem7  49450  toplatglb  49505  setrec1lem2  50192