Theorem uniexd 7691

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

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 5232  ax-un 7684

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 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unexg  7692  iunexg  7911  cofon1  8603  cofon2  8604  axdc2lem  10365  ttukeylem3  10428  ghmqusnsglem1  19250  ghmqusnsg  19252  ghmquskerlem1  19253  ghmquskerco  19254  ghmquskerlem3  19256  ghmqusker  19257  frgpcyg  21567  eltg  22936  ntrval  23015  neiptopnei  23111  neitr  23159  cnpresti  23267  cnprest  23268  lmcnp  23283  uptx  23604  cnextcn  24046  isppw  27095  bdayimaon  27675  nosupno  27685  noinfno  27700  noeta2  27771  etaslts2  27804  cutbdaybnd2lim  27807  oldval  27844  elrspunidl  33507  algextdeglem4  33884  braew  34406  omsfval  34458  omssubaddlem  34463  omssubadd  34464  omsmeas  34487  sibfof  34504  isrrvv  34607  rrvmulc  34617  bnj1489  35218  isfne4  36542  topjoin  36567  mbfresfi  38007  supex2g  38078  restuni4  45575  unirnmap  45661  stoweidlem50  46502  stoweidlem57  46509  stoweidlem59  46511  stoweidlem60  46512  fourierdlem71  46629  intsal  46782  subsaluni  46812  caragenval  46945  omecl  46955  issmflem  47179  issmflelem  47196  issmfle  47197  smfconst  47201  issmfgtlem  47207  issmfgt  47208  issmfgelem  47221  issmfge  47222  smfpimioo  47239  smfresal  47240  fundcmpsurinjlem3  47878  iscnrm3rlem7  49439  toplatglb  49494  setrec1lem2  50181