Theorem uniexd 7744

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

Syntax hints:   → wi 4   ∈ wcel 2150  Vcvv 3462  ∪ cuni 4877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-sep 5262  ax-un 7736

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-v 3464  df-ss 3930  df-uni 4878

This theorem is referenced by:  unexg  7745  iunexg  7963  cofon1  8661  cofon2  8662  axdc2lem  10435  ttukeylem3  10498  ghmqusnsglem1  19353  ghmqusnsg  19355  ghmquskerlem1  19356  ghmquskerco  19357  ghmquskerlem3  19359  ghmqusker  19360  frgpcyg  21706  eltg  23097  ntrval  23176  neiptopnei  23272  neitr  23320  cnpresti  23428  cnprest  23429  lmcnp  23444  uptx  23765  cnextcn  24207  isppw  27258  bdayimaon  27837  nosupno  27847  noinfno  27862  noeta2  27934  etaslts2  27967  cutbdaybnd2lim  27970  oldval  28007  elrspunidl  33706  algextdeglem4  34080  braew  34602  omsfval  34654  omssubaddlem  34659  omssubadd  34660  omsmeas  34683  sibfof  34700  isrrvv  34803  rrvmulc  34813  bnj1489  35414  isfne4  36799  topjoin  36824  mbfresfi  38265  supex2g  38336  restuni4  45791  unirnmap  45876  stoweidlem50  46716  stoweidlem57  46723  stoweidlem59  46725  stoweidlem60  46726  fourierdlem71  46843  intsal  46996  subsaluni  47026  caragenval  47159  omecl  47169  issmflem  47393  issmflelem  47410  issmfle  47411  smfconst  47415  issmfgtlem  47421  issmfgt  47422  issmfgelem  47435  issmfge  47436  smfpimioo  47453  smfresal  47454  fundcmpsurinjlem3  48098  iscnrm3rlem7  49673  toplatglb  49728  setrec1lem2  50415