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

Theorem uniexd 7453
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 7451 . 2 (𝐴𝑉 𝐴 ∈ V)
31, 2syl 17 1 (𝜑 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Vcvv 3469   cuni 4813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-sep 5179  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925  df-uni 4814
This theorem is referenced by:  iunexg  7650  en1b  8564  axdc2lem  9859  ttukeylem3  9922  frgpcyg  20263  eltg  21560  ntrval  21639  neiptopnei  21735  neitr  21783  cnpresti  21891  cnprest  21892  lmcnp  21907  uptx  22228  cnextcn  22670  isppw  25697  braew  31575  omsfval  31626  omssubaddlem  31631  omssubadd  31632  omsmeas  31655  sibfof  31672  isrrvv  31775  rrvmulc  31785  bnj1489  32402  bdayimaon  33271  nosupno  33277  isfne4  33762  topjoin  33787  mbfresfi  35061  supex2g  35133  restuni4  41692  unirnmap  41775  stoweidlem50  42631  stoweidlem57  42638  stoweidlem59  42640  stoweidlem60  42641  fourierdlem71  42758  intsal  42909  subsaluni  42939  caragenval  43071  omecl  43081  issmflem  43300  issmflelem  43317  issmfle  43318  smfconst  43322  issmfgtlem  43328  issmfgt  43329  issmfgelem  43341  issmfge  43342  smfpimioo  43358  smfresal  43359  fundcmpsurinjlem3  43856  setrec1lem2  45157
  Copyright terms: Public domain W3C validator