Theorem uniexd 7741

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464  ∪ cuni 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889

This theorem is referenced by:  unexg  7742  iunexg  7967  cofon1  8689  cofon2  8690  axdc2lem  10467  ttukeylem3  10530  ghmqusnsglem1  19268  ghmqusnsg  19270  ghmquskerlem1  19271  ghmquskerco  19272  ghmquskerlem3  19274  ghmqusker  19275  frgpcyg  21539  eltg  22900  ntrval  22979  neiptopnei  23075  neitr  23123  cnpresti  23231  cnprest  23232  lmcnp  23247  uptx  23568  cnextcn  24010  isppw  27081  bdayimaon  27662  nosupno  27672  noinfno  27687  noeta2  27753  etasslt2  27783  scutbdaybnd2lim  27786  oldval  27819  elrspunidl  33448  algextdeglem4  33759  braew  34278  omsfval  34331  omssubaddlem  34336  omssubadd  34337  omsmeas  34360  sibfof  34377  isrrvv  34480  rrvmulc  34490  bnj1489  35092  isfne4  36363  topjoin  36388  mbfresfi  37695  supex2g  37766  restuni4  45112  unirnmap  45199  stoweidlem50  46046  stoweidlem57  46053  stoweidlem59  46055  stoweidlem60  46056  fourierdlem71  46173  intsal  46326  subsaluni  46356  caragenval  46489  omecl  46499  issmflem  46723  issmflelem  46740  issmfle  46741  smfconst  46745  issmfgtlem  46751  issmfgt  46752  issmfgelem  46765  issmfge  46766  smfpimioo  46783  smfresal  46784  fundcmpsurinjlem3  47381  iscnrm3rlem7  48887  toplatglb  48942  setrec1lem2  49519