Theorem uniexd 7675

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  ∪ cuni 4856

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  unexg  7676  iunexg  7895  cofon1  8587  cofon2  8588  axdc2lem  10339  ttukeylem3  10402  ghmqusnsglem1  19192  ghmqusnsg  19194  ghmquskerlem1  19195  ghmquskerco  19196  ghmquskerlem3  19198  ghmqusker  19199  frgpcyg  21510  eltg  22872  ntrval  22951  neiptopnei  23047  neitr  23095  cnpresti  23203  cnprest  23204  lmcnp  23219  uptx  23540  cnextcn  23982  isppw  27051  bdayimaon  27632  nosupno  27642  noinfno  27657  noeta2  27724  etasslt2  27755  scutbdaybnd2lim  27758  oldval  27795  elrspunidl  33393  algextdeglem4  33733  braew  34255  omsfval  34307  omssubaddlem  34312  omssubadd  34313  omsmeas  34336  sibfof  34353  isrrvv  34456  rrvmulc  34466  bnj1489  35068  isfne4  36384  topjoin  36409  mbfresfi  37705  supex2g  37776  restuni4  45217  unirnmap  45304  stoweidlem50  46147  stoweidlem57  46154  stoweidlem59  46156  stoweidlem60  46157  fourierdlem71  46274  intsal  46427  subsaluni  46457  caragenval  46590  omecl  46600  issmflem  46824  issmflelem  46841  issmfle  46842  smfconst  46846  issmfgtlem  46852  issmfgt  46853  issmfgelem  46866  issmfge  46867  smfpimioo  46884  smfresal  46885  fundcmpsurinjlem3  47499  iscnrm3rlem7  49045  toplatglb  49100  setrec1lem2  49788