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

Theorem uniex 7186
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3408), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
Hypothesis
Ref Expression
uniex.1 𝐴 ∈ V
Assertion
Ref Expression
uniex 𝐴 ∈ V

Proof of Theorem uniex
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniex.1 . 2 𝐴 ∈ V
2 unieq 4645 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
32eleq1d 2877 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
4 uniex2 7185 . . 3 𝑦 𝑦 = 𝑥
54issetri 3411 . 2 𝑥 ∈ V
61, 3, 5vtocl 3459 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2157  Vcvv 3398   cuni 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rex 3109  df-v 3400  df-uni 4638
This theorem is referenced by:  vuniex  7187  unex  7189  iunpw  7211  elxp4  7343  elxp5  7344  1stval  7403  2ndval  7404  fo1st  7421  fo2nd  7422  cnvf1o  7513  brtpos2  7596  ixpsnf1o  8188  dffi3  8579  cnfcom2  8849  cnfcom3lem  8850  cnfcom3  8851  trcl  8854  rankc2  8984  rankxpl  8988  rankxpsuc  8995  acnlem  9157  dfac2a  9238  fin23lem14  9443  fin23lem16  9445  fin23lem17  9448  fin23lem38  9459  fin23lem39  9460  itunisuc  9529  axdc3lem2  9561  axcclem  9567  ac5b  9588  ttukey  9628  wunex2  9848  wuncval2  9857  intgru  9924  pnfxr  10380  prdsval  16323  prdsds  16332  wunfunc  16766  wunnat  16823  arwval  16900  catcfuccl  16966  catcxpccl  17055  zrhval  20067  mreclatdemoBAD  21118  ptbasin2  21599  ptbasfi  21602  dfac14  21639  ptcmplem2  22074  ptcmplem3  22075  ptcmp  22079  cnextfvval  22086  cnextcn  22088  minveclem4a  23419  xrge0tsmsbi  30117  locfinreflem  30238  pstmfval  30270  pstmxmet  30271  esumex  30422  msrval  31763  dfrdg2  32026  trpredex  32062  fvbigcup  32335  ptrest  33723  heiborlem1  33923  heiborlem3  33925  heibor  33933  dicval  36958  aomclem1  38126  dfac21  38138  ntrrn  38921  ntrf  38922  dssmapntrcls  38927  fourierdlem70  40873  caragendifcl  41211  cnfsmf  41432  setrec1lem3  43005  setrec2fun  43008
  Copyright terms: Public domain W3C validator