Theorem uniexd 7747

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

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

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 2734  ax-sep 5255  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  unexg  7748  iunexg  7963  cofon1  8663  cofon2  8664  axdc2lem  10453  ttukeylem3  10516  ghmqusnsglem1  19408  ghmqusnsg  19410  ghmquskerlem1  19411  ghmquskerco  19412  ghmquskerlem3  19414  ghmqusker  19415  frgpcyg  21787  eltg  23183  ntrval  23262  neiptopnei  23358  neitr  23406  cnpresti  23514  cnprest  23515  lmcnp  23530  uptx  23852  cnextcn  24294  isppw  27348  bdayimaon  27927  nosupno  27937  noinfno  27952  noeta2  28024  etaslts2  28057  cutbdaybnd2lim  28060  oldval  28097  elrspunidl  33843  algextdeglem4  34217  braew  34740  omsfval  34792  omssubaddlem  34797  omssubadd  34798  omsmeas  34821  sibfof  34838  isrrvv  34941  rrvmulc  34951  bnj1489  35552  isfne4  36946  topjoin  36971  mbfresfi  38402  supex2g  38474  restuni4  45940  unirnmap  46025  stoweidlem50  46865  stoweidlem57  46872  stoweidlem59  46874  stoweidlem60  46875  fourierdlem71  46992  intsal  47145  subsaluni  47175  caragenval  47308  omecl  47318  issmflem  47542  issmflelem  47559  issmfle  47560  smfconst  47564  issmfgtlem  47570  issmfgt  47571  issmfgelem  47584  issmfge  47585  smfpimioo  47602  smfresal  47603  fundcmpsurinjlem3  48287  iscnrm3rlem7  49859  toplatglb  49914  setrec1lem2  50601