Theorem uniexd 7678

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436  ∪ cuni 4858

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 5235  ax-un 7671

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 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  unexg  7679  iunexg  7898  cofon1  8590  cofon2  8591  axdc2lem  10342  ttukeylem3  10405  ghmqusnsglem1  19159  ghmqusnsg  19161  ghmquskerlem1  19162  ghmquskerco  19163  ghmquskerlem3  19165  ghmqusker  19166  frgpcyg  21480  eltg  22842  ntrval  22921  neiptopnei  23017  neitr  23065  cnpresti  23173  cnprest  23174  lmcnp  23189  uptx  23510  cnextcn  23952  isppw  27022  bdayimaon  27603  nosupno  27613  noinfno  27628  noeta2  27695  etasslt2  27726  scutbdaybnd2lim  27729  oldval  27766  elrspunidl  33374  algextdeglem4  33703  braew  34225  omsfval  34278  omssubaddlem  34283  omssubadd  34284  omsmeas  34307  sibfof  34324  isrrvv  34427  rrvmulc  34437  bnj1489  35039  isfne4  36334  topjoin  36359  mbfresfi  37666  supex2g  37737  restuni4  45119  unirnmap  45206  stoweidlem50  46051  stoweidlem57  46058  stoweidlem59  46060  stoweidlem60  46061  fourierdlem71  46178  intsal  46331  subsaluni  46361  caragenval  46494  omecl  46504  issmflem  46728  issmflelem  46745  issmfle  46746  smfconst  46750  issmfgtlem  46756  issmfgt  46757  issmfgelem  46770  issmfge  46771  smfpimioo  46788  smfresal  46789  fundcmpsurinjlem3  47404  iscnrm3rlem7  48950  toplatglb  49005  setrec1lem2  49693