Theorem uniexd 7685

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 7683	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ 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:  unexg  7686  iunexg  7905  cofon1  8597  cofon2  8598  axdc2lem  10359  ttukeylem3  10422  ghmqusnsglem1  19244  ghmqusnsg  19246  ghmquskerlem1  19247  ghmquskerco  19248  ghmquskerlem3  19250  ghmqusker  19251  frgpcyg  21542  eltg  22910  ntrval  22989  neiptopnei  23085  neitr  23133  cnpresti  23241  cnprest  23242  lmcnp  23257  uptx  23578  cnextcn  24020  isppw  27065  bdayimaon  27645  nosupno  27655  noinfno  27670  noeta2  27741  etaslts2  27774  cutbdaybnd2lim  27777  oldval  27814  elrspunidl  33476  algextdeglem4  33852  braew  34374  omsfval  34426  omssubaddlem  34431  omssubadd  34432  omsmeas  34455  sibfof  34472  isrrvv  34575  rrvmulc  34585  bnj1489  35186  isfne4  36510  topjoin  36535  mbfresfi  37975  supex2g  38046  restuni4  45539  unirnmap  45625  stoweidlem50  46466  stoweidlem57  46473  stoweidlem59  46475  stoweidlem60  46476  fourierdlem71  46593  intsal  46746  subsaluni  46776  caragenval  46909  omecl  46919  issmflem  47143  issmflelem  47160  issmfle  47161  smfconst  47165  issmfgtlem  47171  issmfgt  47172  issmfgelem  47185  issmfge  47186  smfpimioo  47203  smfresal  47204  fundcmpsurinjlem3  47848  iscnrm3rlem7  49409  toplatglb  49464  setrec1lem2  50151