Theorem uniexd 7753

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458  ∪ cuni 4877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878

This theorem is used by:  unexg  7754  iunexg  7969  cofon1  8667  cofon2  8668  axdc2lem  10450  ttukeylem3  10513  ghmqusnsglem1  19375  ghmqusnsg  19377  ghmquskerlem1  19378  ghmquskerco  19379  ghmquskerlem3  19381  ghmqusker  19382  frgpcyg  21753  eltg  23144  ntrval  23223  neiptopnei  23319  neitr  23367  cnpresti  23475  cnprest  23476  lmcnp  23491  uptx  23812  cnextcn  24254  isppw  27308  bdayimaon  27887  nosupno  27897  noinfno  27912  noeta2  27984  etaslts2  28017  cutbdaybnd2lim  28020  oldval  28057  elrspunidl  33760  algextdeglem4  34134  braew  34656  omsfval  34708  omssubaddlem  34713  omssubadd  34714  omsmeas  34737  sibfof  34754  isrrvv  34857  rrvmulc  34867  bnj1489  35468  isfne4  36884  topjoin  36909  mbfresfi  38350  supex2g  38421  restuni4  45872  unirnmap  45957  stoweidlem50  46797  stoweidlem57  46804  stoweidlem59  46806  stoweidlem60  46807  fourierdlem71  46924  intsal  47077  subsaluni  47107  caragenval  47240  omecl  47250  issmflem  47474  issmflelem  47491  issmfle  47492  smfconst  47496  issmfgtlem  47502  issmfgt  47503  issmfgelem  47516  issmfge  47517  smfpimioo  47534  smfresal  47535  fundcmpsurinjlem3  48182  iscnrm3rlem7  49757  toplatglb  49812  setrec1lem2  50499