Theorem uniexd 7470

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496  ∪ cuni 4840

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  iunexg  7666  en1b  8579  axdc2lem  9872  ttukeylem3  9935  frgpcyg  20722  eltg  21567  ntrval  21646  neiptopnei  21742  neitr  21790  cnpresti  21898  cnprest  21899  lmcnp  21914  uptx  22235  cnextcn  22677  isppw  25693  braew  31503  omsfval  31554  omssubaddlem  31559  omssubadd  31560  omsmeas  31583  sibfof  31600  isrrvv  31703  rrvmulc  31713  bnj1489  32330  bdayimaon  33199  nosupno  33205  isfne4  33690  topjoin  33715  mbfresfi  34940  supex2g  35014  restuni4  41394  unirnmap  41478  stoweidlem50  42342  stoweidlem57  42349  stoweidlem59  42351  stoweidlem60  42352  fourierdlem71  42469  intsal  42620  subsaluni  42650  caragenval  42782  omecl  42792  issmflem  43011  issmflelem  43028  issmfle  43029  smfconst  43033  issmfgtlem  43039  issmfgt  43040  issmfgelem  43052  issmfge  43053  smfpimioo  43069  smfresal  43070  fundcmpsurinjlem3  43567  setrec1lem2  44798