Theorem uniexd 7732

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  iunexg  7950  cofon1  8671  cofon2  8672  en1bOLD  9024  axdc2lem  10443  ttukeylem3  10506  frgpcyg  21129  eltg  22460  ntrval  22540  neiptopnei  22636  neitr  22684  cnpresti  22792  cnprest  22793  lmcnp  22808  uptx  23129  cnextcn  23571  isppw  26618  bdayimaon  27196  nosupno  27206  noinfno  27221  noeta2  27286  etasslt2  27316  scutbdaybnd2lim  27319  oldval  27350  ghmquskerlem1  32559  ghmquskerco  32560  ghmquskerlem3  32562  ghmqusker  32563  elrspunidl  32577  algextdeglem1  32803  braew  33271  omsfval  33324  omssubaddlem  33329  omssubadd  33330  omsmeas  33353  sibfof  33370  isrrvv  33473  rrvmulc  33483  bnj1489  34098  isfne4  35273  topjoin  35298  mbfresfi  36582  supex2g  36653  restuni4  43858  unirnmap  43955  stoweidlem50  44814  stoweidlem57  44821  stoweidlem59  44823  stoweidlem60  44824  fourierdlem71  44941  intsal  45094  subsaluni  45124  caragenval  45257  omecl  45267  issmflem  45491  issmflelem  45508  issmfle  45509  smfconst  45513  issmfgtlem  45519  issmfgt  45520  issmfgelem  45533  issmfge  45534  smfpimioo  45551  smfresal  45552  fundcmpsurinjlem3  46116  iscnrm3rlem7  47627  toplatglb  47674  setrec1lem2  47781