MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniexd Structured version   Visualization version   GIF version

Theorem uniexd 7457
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
StepHypRef Expression
1 uniexd.1 . 2 (𝜑𝐴𝑉)
2 uniexg 7456 . 2 (𝐴𝑉 𝐴 ∈ V)
31, 2syl 17 1 (𝜑 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-v 3494  df-uni 4831
This theorem is referenced by:  iunexg  7653  en1b  8565  axdc2lem  9858  ttukeylem3  9921  frgpcyg  20648  eltg  21493  ntrval  21572  neiptopnei  21668  neitr  21716  cnpresti  21824  cnprest  21825  lmcnp  21840  uptx  22161  cnextcn  22603  isppw  25618  braew  31400  omsfval  31451  omssubaddlem  31456  omssubadd  31457  omsmeas  31480  sibfof  31497  isrrvv  31600  rrvmulc  31610  bnj1489  32225  bdayimaon  33094  nosupno  33100  isfne4  33585  topjoin  33610  mbfresfi  34819  supex2g  34893  restuni4  41264  unirnmap  41347  stoweidlem50  42212  stoweidlem57  42219  stoweidlem59  42221  stoweidlem60  42222  fourierdlem71  42339  intsal  42490  subsaluni  42520  caragenval  42652  omecl  42662  issmflem  42881  issmflelem  42898  issmfle  42899  smfconst  42903  issmfgtlem  42909  issmfgt  42910  issmfgelem  42922  issmfge  42923  smfpimioo  42939  smfresal  42940  fundcmpsurinjlem3  43437  setrec1lem2  44719
  Copyright terms: Public domain W3C validator