Theorem uniexd 7718

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  ∪ cuni 4871

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 5251  ax-un 7711

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 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unexg  7719  iunexg  7942  cofon1  8636  cofon2  8637  axdc2lem  10401  ttukeylem3  10464  ghmqusnsglem1  19212  ghmqusnsg  19214  ghmquskerlem1  19215  ghmquskerco  19216  ghmquskerlem3  19218  ghmqusker  19219  frgpcyg  21483  eltg  22844  ntrval  22923  neiptopnei  23019  neitr  23067  cnpresti  23175  cnprest  23176  lmcnp  23191  uptx  23512  cnextcn  23954  isppw  27024  bdayimaon  27605  nosupno  27615  noinfno  27630  noeta2  27696  etasslt2  27726  scutbdaybnd2lim  27729  oldval  27762  elrspunidl  33399  algextdeglem4  33710  braew  34232  omsfval  34285  omssubaddlem  34290  omssubadd  34291  omsmeas  34314  sibfof  34331  isrrvv  34434  rrvmulc  34444  bnj1489  35046  isfne4  36328  topjoin  36353  mbfresfi  37660  supex2g  37731  restuni4  45115  unirnmap  45202  stoweidlem50  46048  stoweidlem57  46055  stoweidlem59  46057  stoweidlem60  46058  fourierdlem71  46175  intsal  46328  subsaluni  46358  caragenval  46491  omecl  46501  issmflem  46725  issmflelem  46742  issmfle  46743  smfconst  46747  issmfgtlem  46753  issmfgt  46754  issmfgelem  46767  issmfge  46768  smfpimioo  46785  smfresal  46786  fundcmpsurinjlem3  47398  iscnrm3rlem7  48931  toplatglb  48986  setrec1lem2  49674