Theorem uniexd 7762

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  ∪ cuni 4907

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unexg  7763  iunexg  7988  cofon1  8710  cofon2  8711  axdc2lem  10488  ttukeylem3  10551  ghmqusnsglem1  19298  ghmqusnsg  19300  ghmquskerlem1  19301  ghmquskerco  19302  ghmquskerlem3  19304  ghmqusker  19305  frgpcyg  21592  eltg  22964  ntrval  23044  neiptopnei  23140  neitr  23188  cnpresti  23296  cnprest  23297  lmcnp  23312  uptx  23633  cnextcn  24075  isppw  27157  bdayimaon  27738  nosupno  27748  noinfno  27763  noeta2  27829  etasslt2  27859  scutbdaybnd2lim  27862  oldval  27893  elrspunidl  33456  algextdeglem4  33761  braew  34243  omsfval  34296  omssubaddlem  34301  omssubadd  34302  omsmeas  34325  sibfof  34342  isrrvv  34445  rrvmulc  34455  bnj1489  35070  isfne4  36341  topjoin  36366  mbfresfi  37673  supex2g  37744  restuni4  45126  unirnmap  45213  stoweidlem50  46065  stoweidlem57  46072  stoweidlem59  46074  stoweidlem60  46075  fourierdlem71  46192  intsal  46345  subsaluni  46375  caragenval  46508  omecl  46518  issmflem  46742  issmflelem  46759  issmfle  46760  smfconst  46764  issmfgtlem  46770  issmfgt  46771  issmfgelem  46784  issmfge  46785  smfpimioo  46802  smfresal  46803  fundcmpsurinjlem3  47387  iscnrm3rlem7  48843  toplatglb  48890  setrec1lem2  49207