Theorem uniexd 7448

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  iunexg  7646  en1b  8560  axdc2lem  9859  ttukeylem3  9922  frgpcyg  20265  eltg  21562  ntrval  21641  neiptopnei  21737  neitr  21785  cnpresti  21893  cnprest  21894  lmcnp  21909  uptx  22230  cnextcn  22672  isppw  25699  elrspunidl  31014  braew  31611  omsfval  31662  omssubaddlem  31667  omssubadd  31668  omsmeas  31691  sibfof  31708  isrrvv  31811  rrvmulc  31821  bnj1489  32438  bdayimaon  33310  nosupno  33316  isfne4  33801  topjoin  33826  mbfresfi  35103  supex2g  35175  restuni4  41756  unirnmap  41837  stoweidlem50  42692  stoweidlem57  42699  stoweidlem59  42701  stoweidlem60  42702  fourierdlem71  42819  intsal  42970  subsaluni  43000  caragenval  43132  omecl  43142  issmflem  43361  issmflelem  43378  issmfle  43379  smfconst  43383  issmfgtlem  43389  issmfgt  43390  issmfgelem  43402  issmfge  43403  smfpimioo  43419  smfresal  43420  fundcmpsurinjlem3  43917  setrec1lem2  45218