Theorem uniexd 7670

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3434  ∪ cuni 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-ss 3917  df-uni 4858

This theorem is referenced by:  unexg  7671  iunexg  7890  cofon1  8582  cofon2  8583  axdc2lem  10331  ttukeylem3  10394  ghmqusnsglem1  19185  ghmqusnsg  19187  ghmquskerlem1  19188  ghmquskerco  19189  ghmquskerlem3  19191  ghmqusker  19192  frgpcyg  21503  eltg  22865  ntrval  22944  neiptopnei  23040  neitr  23088  cnpresti  23196  cnprest  23197  lmcnp  23212  uptx  23533  cnextcn  23975  isppw  27044  bdayimaon  27625  nosupno  27635  noinfno  27650  noeta2  27717  etasslt2  27748  scutbdaybnd2lim  27751  oldval  27788  elrspunidl  33383  algextdeglem4  33723  braew  34245  omsfval  34297  omssubaddlem  34302  omssubadd  34303  omsmeas  34326  sibfof  34343  isrrvv  34446  rrvmulc  34456  bnj1489  35058  isfne4  36353  topjoin  36378  mbfresfi  37685  supex2g  37756  restuni4  45137  unirnmap  45224  stoweidlem50  46067  stoweidlem57  46074  stoweidlem59  46076  stoweidlem60  46077  fourierdlem71  46194  intsal  46347  subsaluni  46377  caragenval  46510  omecl  46520  issmflem  46744  issmflelem  46761  issmfle  46762  smfconst  46766  issmfgtlem  46772  issmfgt  46773  issmfgelem  46786  issmfge  46787  smfpimioo  46804  smfresal  46805  fundcmpsurinjlem3  47410  iscnrm3rlem7  48956  toplatglb  49011  setrec1lem2  49699