Theorem uniexd 7777

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unexg  7778  iunexg  8004  cofon1  8728  cofon2  8729  en1bOLD  9089  axdc2lem  10517  ttukeylem3  10580  ghmqusnsglem1  19320  ghmqusnsg  19322  ghmquskerlem1  19323  ghmquskerco  19324  ghmquskerlem3  19326  ghmqusker  19327  frgpcyg  21615  eltg  22985  ntrval  23065  neiptopnei  23161  neitr  23209  cnpresti  23317  cnprest  23318  lmcnp  23333  uptx  23654  cnextcn  24096  isppw  27175  bdayimaon  27756  nosupno  27766  noinfno  27781  noeta2  27847  etasslt2  27877  scutbdaybnd2lim  27880  oldval  27911  elrspunidl  33421  algextdeglem4  33711  braew  34206  omsfval  34259  omssubaddlem  34264  omssubadd  34265  omsmeas  34288  sibfof  34305  isrrvv  34408  rrvmulc  34418  bnj1489  35032  isfne4  36306  topjoin  36331  mbfresfi  37626  supex2g  37697  restuni4  45023  unirnmap  45115  stoweidlem50  45971  stoweidlem57  45978  stoweidlem59  45980  stoweidlem60  45981  fourierdlem71  46098  intsal  46251  subsaluni  46281  caragenval  46414  omecl  46424  issmflem  46648  issmflelem  46665  issmfle  46666  smfconst  46670  issmfgtlem  46676  issmfgt  46677  issmfgelem  46690  issmfge  46691  smfpimioo  46708  smfresal  46709  fundcmpsurinjlem3  47274  iscnrm3rlem7  48626  toplatglb  48673  setrec1lem2  48780