Theorem uniexd 7755

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3462  ∪ cuni 4915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5306  ax-un 7748

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-uni 4916

This theorem is referenced by:  iunexg  7979  cofon1  8704  cofon2  8705  en1bOLD  9062  axdc2lem  10493  ttukeylem3  10556  ghmqusnsglem1  19276  ghmqusnsg  19278  ghmquskerlem1  19279  ghmquskerco  19280  ghmquskerlem3  19282  ghmqusker  19283  frgpcyg  21573  eltg  22954  ntrval  23034  neiptopnei  23130  neitr  23178  cnpresti  23286  cnprest  23287  lmcnp  23302  uptx  23623  cnextcn  24065  isppw  27145  bdayimaon  27726  nosupno  27736  noinfno  27751  noeta2  27817  etasslt2  27847  scutbdaybnd2lim  27850  oldval  27881  elrspunidl  33305  algextdeglem4  33589  braew  34077  omsfval  34130  omssubaddlem  34135  omssubadd  34136  omsmeas  34159  sibfof  34176  isrrvv  34279  rrvmulc  34289  bnj1489  34903  isfne4  36054  topjoin  36079  mbfresfi  37369  supex2g  37440  restuni4  44740  unirnmap  44833  stoweidlem50  45689  stoweidlem57  45696  stoweidlem59  45698  stoweidlem60  45699  fourierdlem71  45816  intsal  45969  subsaluni  45999  caragenval  46132  omecl  46142  issmflem  46366  issmflelem  46383  issmfle  46384  smfconst  46388  issmfgtlem  46394  issmfgt  46395  issmfgelem  46408  issmfge  46409  smfpimioo  46426  smfresal  46427  fundcmpsurinjlem3  46990  iscnrm3rlem7  48298  toplatglb  48345  setrec1lem2  48452