Theorem uniexd 7595

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  iunexg  7806  en1bOLD  8814  axdc2lem  10204  ttukeylem3  10267  frgpcyg  20781  eltg  22107  ntrval  22187  neiptopnei  22283  neitr  22331  cnpresti  22439  cnprest  22440  lmcnp  22455  uptx  22776  cnextcn  23218  isppw  26263  elrspunidl  31606  braew  32210  omsfval  32261  omssubaddlem  32266  omssubadd  32267  omsmeas  32290  sibfof  32307  isrrvv  32410  rrvmulc  32420  bnj1489  33036  bdayimaon  33896  nosupno  33906  noinfno  33921  noeta2  33979  etasslt2  34008  scutbdaybnd2lim  34011  oldval  34038  isfne4  34529  topjoin  34554  mbfresfi  35823  supex2g  35895  restuni4  42670  unirnmap  42748  stoweidlem50  43591  stoweidlem57  43598  stoweidlem59  43600  stoweidlem60  43601  fourierdlem71  43718  intsal  43869  subsaluni  43899  caragenval  44031  omecl  44041  issmflem  44263  issmflelem  44280  issmfle  44281  smfconst  44285  issmfgtlem  44291  issmfgt  44292  issmfgelem  44304  issmfge  44305  smfpimioo  44321  smfresal  44322  fundcmpsurinjlem3  44852  iscnrm3rlem7  46240  toplatglb  46287  setrec1lem2  46394