Theorem uniexd 7727

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868

This theorem is referenced by:  unexg  7728  iunexg  7946  cofon1  8644  cofon2  8645  axdc2lem  10407  ttukeylem3  10470  ghmqusnsglem1  19322  ghmqusnsg  19324  ghmquskerlem1  19325  ghmquskerco  19326  ghmquskerlem3  19328  ghmqusker  19329  frgpcyg  21627  eltg  23019  ntrval  23098  neiptopnei  23194  neitr  23242  cnpresti  23350  cnprest  23351  lmcnp  23366  uptx  23687  cnextcn  24129  isppw  27180  bdayimaon  27759  nosupno  27769  noinfno  27784  noeta2  27856  etaslts2  27889  cutbdaybnd2lim  27892  oldval  27929  elrspunidl  33616  algextdeglem4  34019  braew  34541  omsfval  34593  omssubaddlem  34598  omssubadd  34599  omsmeas  34622  sibfof  34639  isrrvv  34742  rrvmulc  34752  bnj1489  35353  isfne4  36705  topjoin  36730  mbfresfi  38170  supex2g  38241  restuni4  45704  unirnmap  45789  stoweidlem50  46629  stoweidlem57  46636  stoweidlem59  46638  stoweidlem60  46639  fourierdlem71  46756  intsal  46909  subsaluni  46939  caragenval  47072  omecl  47082  issmflem  47306  issmflelem  47323  issmfle  47324  smfconst  47328  issmfgtlem  47334  issmfgt  47335  issmfgelem  47348  issmfge  47349  smfpimioo  47366  smfresal  47367  fundcmpsurinjlem3  48011  iscnrm3rlem7  49572  toplatglb  49627  setrec1lem2  50314