Theorem uniexd 7689

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865

This theorem is referenced by:  unexg  7690  iunexg  7909  cofon1  8602  cofon2  8603  axdc2lem  10362  ttukeylem3  10425  ghmqusnsglem1  19213  ghmqusnsg  19215  ghmquskerlem1  19216  ghmquskerco  19217  ghmquskerlem3  19219  ghmqusker  19220  frgpcyg  21532  eltg  22905  ntrval  22984  neiptopnei  23080  neitr  23128  cnpresti  23236  cnprest  23237  lmcnp  23252  uptx  23573  cnextcn  24015  isppw  27084  bdayimaon  27665  nosupno  27675  noinfno  27690  noeta2  27761  etaslts2  27794  cutbdaybnd2lim  27797  oldval  27834  elrspunidl  33511  algextdeglem4  33879  braew  34401  omsfval  34453  omssubaddlem  34458  omssubadd  34459  omsmeas  34482  sibfof  34499  isrrvv  34602  rrvmulc  34612  bnj1489  35214  isfne4  36536  topjoin  36561  mbfresfi  37869  supex2g  37940  restuni4  45432  unirnmap  45519  stoweidlem50  46361  stoweidlem57  46368  stoweidlem59  46370  stoweidlem60  46371  fourierdlem71  46488  intsal  46641  subsaluni  46671  caragenval  46804  omecl  46814  issmflem  47038  issmflelem  47055  issmfle  47056  smfconst  47060  issmfgtlem  47066  issmfgt  47067  issmfgelem  47080  issmfge  47081  smfpimioo  47098  smfresal  47099  fundcmpsurinjlem3  47713  iscnrm3rlem7  49258  toplatglb  49313  setrec1lem2  50000