Theorem uniexd 7698

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unexg  7699  iunexg  7921  cofon1  8613  cofon2  8614  axdc2lem  10379  ttukeylem3  10442  ghmqusnsglem1  19195  ghmqusnsg  19197  ghmquskerlem1  19198  ghmquskerco  19199  ghmquskerlem3  19201  ghmqusker  19202  frgpcyg  21516  eltg  22878  ntrval  22957  neiptopnei  23053  neitr  23101  cnpresti  23209  cnprest  23210  lmcnp  23225  uptx  23546  cnextcn  23988  isppw  27058  bdayimaon  27639  nosupno  27649  noinfno  27664  noeta2  27731  etasslt2  27761  scutbdaybnd2lim  27764  oldval  27800  elrspunidl  33393  algextdeglem4  33704  braew  34226  omsfval  34279  omssubaddlem  34284  omssubadd  34285  omsmeas  34308  sibfof  34325  isrrvv  34428  rrvmulc  34438  bnj1489  35040  isfne4  36322  topjoin  36347  mbfresfi  37654  supex2g  37725  restuni4  45109  unirnmap  45196  stoweidlem50  46042  stoweidlem57  46049  stoweidlem59  46051  stoweidlem60  46052  fourierdlem71  46169  intsal  46322  subsaluni  46352  caragenval  46485  omecl  46495  issmflem  46719  issmflelem  46736  issmfle  46737  smfconst  46741  issmfgtlem  46747  issmfgt  46748  issmfgelem  46761  issmfge  46762  smfpimioo  46779  smfresal  46780  fundcmpsurinjlem3  47395  iscnrm3rlem7  48928  toplatglb  48983  setrec1lem2  49671