Theorem uniexd 7649

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3441  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-un 7642

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3904  df-ss 3914  df-uni 4852

This theorem is referenced by:  iunexg  7866  en1bOLD  8881  axdc2lem  10297  ttukeylem3  10360  frgpcyg  20879  eltg  22205  ntrval  22285  neiptopnei  22381  neitr  22429  cnpresti  22537  cnprest  22538  lmcnp  22553  uptx  22874  cnextcn  23316  isppw  26361  bdayimaon  26939  nosupno  26949  noinfno  26964  elrspunidl  31844  braew  32449  omsfval  32502  omssubaddlem  32507  omssubadd  32508  omsmeas  32531  sibfof  32548  isrrvv  32651  rrvmulc  32661  bnj1489  33276  noeta2  34070  etasslt2  34099  scutbdaybnd2lim  34102  oldval  34129  isfne4  34620  topjoin  34645  mbfresfi  35921  supex2g  35993  restuni4  42980  unirnmap  43064  stoweidlem50  43916  stoweidlem57  43923  stoweidlem59  43925  stoweidlem60  43926  fourierdlem71  44043  intsal  44194  subsaluni  44224  caragenval  44357  omecl  44367  issmflem  44591  issmflelem  44608  issmfle  44609  smfconst  44613  issmfgtlem  44619  issmfgt  44620  issmfgelem  44633  issmfge  44634  smfpimioo  44651  smfresal  44652  fundcmpsurinjlem3  45192  iscnrm3rlem7  46580  toplatglb  46627  setrec1lem2  46734