Theorem uniexd 7760

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  unexg  7761  iunexg  7986  cofon1  8708  cofon2  8709  axdc2lem  10485  ttukeylem3  10548  ghmqusnsglem1  19310  ghmqusnsg  19312  ghmquskerlem1  19313  ghmquskerco  19314  ghmquskerlem3  19316  ghmqusker  19317  frgpcyg  21609  eltg  22979  ntrval  23059  neiptopnei  23155  neitr  23203  cnpresti  23311  cnprest  23312  lmcnp  23327  uptx  23648  cnextcn  24090  isppw  27171  bdayimaon  27752  nosupno  27762  noinfno  27777  noeta2  27843  etasslt2  27873  scutbdaybnd2lim  27876  oldval  27907  elrspunidl  33435  algextdeglem4  33725  braew  34222  omsfval  34275  omssubaddlem  34280  omssubadd  34281  omsmeas  34304  sibfof  34321  isrrvv  34424  rrvmulc  34434  bnj1489  35048  isfne4  36322  topjoin  36347  mbfresfi  37652  supex2g  37723  restuni4  45060  unirnmap  45150  stoweidlem50  46005  stoweidlem57  46012  stoweidlem59  46014  stoweidlem60  46015  fourierdlem71  46132  intsal  46285  subsaluni  46315  caragenval  46448  omecl  46458  issmflem  46682  issmflelem  46699  issmfle  46700  smfconst  46704  issmfgtlem  46710  issmfgt  46711  issmfgelem  46724  issmfge  46725  smfpimioo  46742  smfresal  46743  fundcmpsurinjlem3  47324  iscnrm3rlem7  48742  toplatglb  48789  setrec1lem2  48918