Theorem uniexd 7699

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unexg  7700  iunexg  7919  cofon1  8612  cofon2  8613  axdc2lem  10372  ttukeylem3  10435  ghmqusnsglem1  19226  ghmqusnsg  19228  ghmquskerlem1  19229  ghmquskerco  19230  ghmquskerlem3  19232  ghmqusker  19233  frgpcyg  21545  eltg  22918  ntrval  22997  neiptopnei  23093  neitr  23141  cnpresti  23249  cnprest  23250  lmcnp  23265  uptx  23586  cnextcn  24028  isppw  27097  bdayimaon  27678  nosupno  27688  noinfno  27703  noeta2  27774  etaslts2  27807  cutbdaybnd2lim  27810  oldval  27847  elrspunidl  33527  algextdeglem4  33904  braew  34426  omsfval  34478  omssubaddlem  34483  omssubadd  34484  omsmeas  34507  sibfof  34524  isrrvv  34627  rrvmulc  34637  bnj1489  35238  isfne4  36562  topjoin  36587  mbfresfi  37946  supex2g  38017  restuni4  45509  unirnmap  45595  stoweidlem50  46437  stoweidlem57  46444  stoweidlem59  46446  stoweidlem60  46447  fourierdlem71  46564  intsal  46717  subsaluni  46747  caragenval  46880  omecl  46890  issmflem  47114  issmflelem  47131  issmfle  47132  smfconst  47136  issmfgtlem  47142  issmfgt  47143  issmfgelem  47156  issmfge  47157  smfpimioo  47174  smfresal  47175  fundcmpsurinjlem3  47789  iscnrm3rlem7  49334  toplatglb  49389  setrec1lem2  50076