Theorem uniexd 7742

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454  ∪ cuni 4871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872

This theorem is used by:  unexg  7743  iunexg  7958  cofon1  8656  cofon2  8657  axdc2lem  10438  ttukeylem3  10501  ghmqusnsglem1  19356  ghmqusnsg  19358  ghmquskerlem1  19359  ghmquskerco  19360  ghmquskerlem3  19362  ghmqusker  19363  frgpcyg  21734  eltg  23125  ntrval  23204  neiptopnei  23300  neitr  23348  cnpresti  23456  cnprest  23457  lmcnp  23472  uptx  23793  cnextcn  24235  isppw  27289  bdayimaon  27868  nosupno  27878  noinfno  27893  noeta2  27965  etaslts2  27998  cutbdaybnd2lim  28001  oldval  28038  elrspunidl  33745  algextdeglem4  34119  braew  34641  omsfval  34693  omssubaddlem  34698  omssubadd  34699  omsmeas  34722  sibfof  34739  isrrvv  34842  rrvmulc  34852  bnj1489  35453  isfne4  36879  topjoin  36904  mbfresfi  38345  supex2g  38416  restuni4  45867  unirnmap  45952  stoweidlem50  46792  stoweidlem57  46799  stoweidlem59  46801  stoweidlem60  46802  fourierdlem71  46919  intsal  47072  subsaluni  47102  caragenval  47235  omecl  47245  issmflem  47469  issmflelem  47486  issmfle  47487  smfconst  47491  issmfgtlem  47497  issmfgt  47498  issmfgelem  47511  issmfge  47512  smfpimioo  47529  smfresal  47530  fundcmpsurinjlem3  48177  iscnrm3rlem7  49752  toplatglb  49807  setrec1lem2  50494