Theorem uniexd 7759

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  unexg  7760  iunexg  7975  cofon1  8681  cofon2  8682  setrec1lem2  9967  axdc2lem  10526  ttukeylem3  10589  ghmqusnsglem1  19494  ghmqusnsg  19496  ghmquskerlem1  19497  ghmquskerco  19498  ghmquskerlem3  19500  ghmqusker  19501  frgpcyg  21879  eltg  23275  ntrval  23354  neiptopnei  23450  neitr  23498  cnpresti  23606  cnprest  23607  lmcnp  23622  uptx  23944  cnextcn  24386  isppw  27441  bdayimaon  28050  nosupno  28060  noinfno  28075  noeta2  28147  etaslts2  28180  cutbdaybnd2lim  28183  oldval  28220  elrspunidl  33978  algextdeglem4  34352  braew  34875  omsfval  34926  omssubaddlem  34931  omssubadd  34932  omsmeas  34955  sibfof  34972  isrrvv  35075  rrvmulc  35085  bnj1489  35686  isfne4  37128  topjoin  37153  mbfresfi  38585  supex2g  38672  restuni4  46136  unirnmap  46221  stoweidlem50  47060  stoweidlem57  47067  stoweidlem59  47069  stoweidlem60  47070  fourierdlem71  47187  intsal  47340  subsaluni  47370  caragenval  47503  omecl  47513  issmflem  47737  issmflelem  47754  issmfle  47755  smfconst  47759  issmfgtlem  47765  issmfgt  47766  issmfgelem  47779  issmfge  47780  smfpimioo  47797  smfresal  47798  fundcmpsurinjlem3  48482  iscnrm3rlem7  50054  toplatglb  50109