Theorem uniexd 7687

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439  ∪ cuni 4862

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 5240  ax-un 7680

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 3441  df-ss 3917  df-uni 4863

This theorem is referenced by:  unexg  7688  iunexg  7907  cofon1  8600  cofon2  8601  axdc2lem  10360  ttukeylem3  10423  ghmqusnsglem1  19211  ghmqusnsg  19213  ghmquskerlem1  19214  ghmquskerco  19215  ghmquskerlem3  19217  ghmqusker  19218  frgpcyg  21530  eltg  22903  ntrval  22982  neiptopnei  23078  neitr  23126  cnpresti  23234  cnprest  23235  lmcnp  23250  uptx  23571  cnextcn  24013  isppw  27082  bdayimaon  27663  nosupno  27673  noinfno  27688  noeta2  27759  etasslt2  27790  scutbdaybnd2lim  27793  oldval  27830  elrspunidl  33488  algextdeglem4  33856  braew  34378  omsfval  34430  omssubaddlem  34435  omssubadd  34436  omsmeas  34459  sibfof  34476  isrrvv  34579  rrvmulc  34589  bnj1489  35191  isfne4  36513  topjoin  36538  mbfresfi  37836  supex2g  37907  restuni4  45402  unirnmap  45489  stoweidlem50  46331  stoweidlem57  46338  stoweidlem59  46340  stoweidlem60  46341  fourierdlem71  46458  intsal  46611  subsaluni  46641  caragenval  46774  omecl  46784  issmflem  47008  issmflelem  47025  issmfle  47026  smfconst  47030  issmfgtlem  47036  issmfgt  47037  issmfgelem  47050  issmfge  47051  smfpimioo  47068  smfresal  47069  fundcmpsurinjlem3  47683  iscnrm3rlem7  49228  toplatglb  49283  setrec1lem2  49970