Theorem uniexd 7573

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  iunexg  7779  en1bOLD  8768  axdc2lem  10135  ttukeylem3  10198  frgpcyg  20693  eltg  22015  ntrval  22095  neiptopnei  22191  neitr  22239  cnpresti  22347  cnprest  22348  lmcnp  22363  uptx  22684  cnextcn  23126  isppw  26168  elrspunidl  31508  braew  32110  omsfval  32161  omssubaddlem  32166  omssubadd  32167  omsmeas  32190  sibfof  32207  isrrvv  32310  rrvmulc  32320  bnj1489  32936  bdayimaon  33823  nosupno  33833  noinfno  33848  noeta2  33906  etasslt2  33935  scutbdaybnd2lim  33938  oldval  33965  isfne4  34456  topjoin  34481  mbfresfi  35750  supex2g  35822  restuni4  42559  unirnmap  42637  stoweidlem50  43481  stoweidlem57  43488  stoweidlem59  43490  stoweidlem60  43491  fourierdlem71  43608  intsal  43759  subsaluni  43789  caragenval  43921  omecl  43931  issmflem  44150  issmflelem  44167  issmfle  44168  smfconst  44172  issmfgtlem  44178  issmfgt  44179  issmfgelem  44191  issmfge  44192  smfpimioo  44208  smfresal  44209  fundcmpsurinjlem3  44740  iscnrm3rlem7  46128  toplatglb  46175  setrec1lem2  46280