Theorem uniexd 7743

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  unexg  7744  iunexg  7959  cofon1  8660  cofon2  8661  setrec1lem2  9924  axdc2lem  10483  ttukeylem3  10546  ghmqusnsglem1  19441  ghmqusnsg  19443  ghmquskerlem1  19444  ghmquskerco  19445  ghmquskerlem3  19447  ghmqusker  19448  frgpcyg  21826  eltg  23222  ntrval  23301  neiptopnei  23397  neitr  23445  cnpresti  23553  cnprest  23554  lmcnp  23569  uptx  23891  cnextcn  24333  isppw  27390  bdayimaon  27969  nosupno  27979  noinfno  27994  noeta2  28066  etaslts2  28099  cutbdaybnd2lim  28102  oldval  28139  elrspunidl  33897  algextdeglem4  34271  braew  34794  omsfval  34846  omssubaddlem  34851  omssubadd  34852  omsmeas  34875  sibfof  34892  isrrvv  34995  rrvmulc  35005  bnj1489  35606  isfne4  37044  topjoin  37069  mbfresfi  38498  supex2g  38585  restuni4  46051  unirnmap  46136  stoweidlem50  46976  stoweidlem57  46983  stoweidlem59  46985  stoweidlem60  46986  fourierdlem71  47103  intsal  47256  subsaluni  47286  caragenval  47419  omecl  47429  issmflem  47653  issmflelem  47670  issmfle  47671  smfconst  47675  issmfgtlem  47681  issmfgt  47682  issmfgelem  47695  issmfge  47696  smfpimioo  47713  smfresal  47714  fundcmpsurinjlem3  48398  iscnrm3rlem7  49970  toplatglb  50025