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  27315  scutbdaybnd2lim  27318  oldval  27349  ghmquskerlem1  32528  ghmquskerco  32529  ghmquskerlem3  32531  ghmqusker  32532  elrspunidl  32546  algextdeglem1  32772  braew  33240  omsfval  33293  omssubaddlem  33298  omssubadd  33299  omsmeas  33322  sibfof  33339  isrrvv  33442  rrvmulc  33452  bnj1489  34067  isfne4  35225  topjoin  35250  mbfresfi  36534  supex2g  36605  restuni4  43810  unirnmap  43907  stoweidlem50  44766  stoweidlem57  44773  stoweidlem59  44775  stoweidlem60  44776  fourierdlem71  44893  intsal  45046  subsaluni  45076  caragenval  45209  omecl  45219  issmflem  45443  issmflelem  45460  issmfle  45461  smfconst  45465  issmfgtlem  45471  issmfgt  45472  issmfgelem  45485  issmfge  45486  smfpimioo  45503  smfresal  45504  fundcmpsurinjlem3  46068  iscnrm3rlem7  47579  toplatglb  47626  setrec1lem2  47733