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  10377  ttukeylem3  10440  ghmqusnsglem1  19194  ghmqusnsg  19196  ghmquskerlem1  19197  ghmquskerco  19198  ghmquskerlem3  19200  ghmqusker  19201  frgpcyg  21515  eltg  22877  ntrval  22956  neiptopnei  23052  neitr  23100  cnpresti  23208  cnprest  23209  lmcnp  23224  uptx  23545  cnextcn  23987  isppw  27057  bdayimaon  27638  nosupno  27648  noinfno  27663  noeta2  27730  etasslt2  27760  scutbdaybnd2lim  27763  oldval  27799  elrspunidl  33392  algextdeglem4  33703  braew  34225  omsfval  34278  omssubaddlem  34283  omssubadd  34284  omsmeas  34307  sibfof  34324  isrrvv  34427  rrvmulc  34437  bnj1489  35039  isfne4  36321  topjoin  36346  mbfresfi  37653  supex2g  37724  restuni4  45108  unirnmap  45195  stoweidlem50  46041  stoweidlem57  46048  stoweidlem59  46050  stoweidlem60  46051  fourierdlem71  46168  intsal  46321  subsaluni  46351  caragenval  46484  omecl  46494  issmflem  46718  issmflelem  46735  issmfle  46736  smfconst  46740  issmfgtlem  46746  issmfgt  46747  issmfgelem  46760  issmfge  46761  smfpimioo  46778  smfresal  46779  fundcmpsurinjlem3  47394  iscnrm3rlem7  48927  toplatglb  48982  setrec1lem2  49670