Theorem uniexd 7780

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  unexg  7781  iunexg  7996  cofon1  8706  cofon2  8707  setrec1lem2  9991  axdc2lem  10550  ttukeylem3  10613  ghmqusnsglem1  19521  ghmqusnsg  19523  ghmquskerlem1  19524  ghmquskerco  19525  ghmquskerlem3  19527  ghmqusker  19528  frgpcyg  21906  eltg  23302  ntrval  23381  neiptopnei  23477  neitr  23525  cnpresti  23633  cnprest  23634  lmcnp  23649  uptx  23971  cnextcn  24413  isppw  27468  bdayimaon  28077  nosupno  28087  noinfno  28102  noeta2  28174  etaslts2  28207  cutbdaybnd2lim  28210  oldval  28247  elrspunidl  34045  algextdeglem4  34419  braew  34942  omsfval  34993  omssubaddlem  34998  omssubadd  34999  omsmeas  35022  sibfof  35039  isrrvv  35142  rrvmulc  35152  bnj1489  35753  isfne4  37305  topjoin  37330  mbfresfi  38775  supex2g  38862  restuni4  46339  unirnmap  46424  stoweidlem50  47263  stoweidlem57  47270  stoweidlem59  47272  stoweidlem60  47273  fourierdlem71  47390  intsal  47543  subsaluni  47573  caragenval  47706  omecl  47716  issmflem  47940  issmflelem  47957  issmfle  47958  smfconst  47962  issmfgtlem  47968  issmfgt  47969  issmfgelem  47982  issmfge  47983  smfpimioo  48000  smfresal  48001  fundcmpsurinjlem3  48685  iscnrm3rlem7  50263  toplatglb  50318