Theorem uniexd 7684

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446  ∪ cuni 4870

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871

This theorem is referenced by:  iunexg  7901  cofon1  8623  cofon2  8624  en1bOLD  8975  axdc2lem  10393  ttukeylem3  10456  frgpcyg  21017  eltg  22344  ntrval  22424  neiptopnei  22520  neitr  22568  cnpresti  22676  cnprest  22677  lmcnp  22692  uptx  23013  cnextcn  23455  isppw  26500  bdayimaon  27078  nosupno  27088  noinfno  27103  noeta2  27167  etasslt2  27196  scutbdaybnd2lim  27199  oldval  27227  ghmquskerlem1  32269  ghmquskerco  32270  ghmqusker  32272  elrspunidl  32279  braew  32930  omsfval  32983  omssubaddlem  32988  omssubadd  32989  omsmeas  33012  sibfof  33029  isrrvv  33132  rrvmulc  33142  bnj1489  33757  isfne4  34888  topjoin  34913  mbfresfi  36197  supex2g  36269  restuni4  43453  unirnmap  43550  stoweidlem50  44411  stoweidlem57  44418  stoweidlem59  44420  stoweidlem60  44421  fourierdlem71  44538  intsal  44691  subsaluni  44721  caragenval  44854  omecl  44864  issmflem  45088  issmflelem  45105  issmfle  45106  smfconst  45110  issmfgtlem  45116  issmfgt  45117  issmfgelem  45130  issmfge  45131  smfpimioo  45148  smfresal  45149  fundcmpsurinjlem3  45712  iscnrm3rlem7  47099  toplatglb  47146  setrec1lem2  47253