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

Theorem uniex 6851
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3180), 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 4380 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
32eleq1d 2672 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
4 uniex2 6850 . . 3 𝑦 𝑦 = 𝑥
54issetri 3183 . 2 𝑥 ∈ V
61, 3, 5vtocl 3232 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wcel 1977  Vcvv 3173   cuni 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-uni 4373
This theorem is referenced by:  vuniex  6852  unex  6854  iunpw  6870  elxp4  7003  elxp5  7004  1stval  7061  2ndval  7062  fo1st  7079  fo2nd  7080  cnvf1o  7163  brtpos2  7245  ixpsnf1o  7834  dffi3  8220  cnfcom2  8482  cnfcom3lem  8483  cnfcom3  8484  trcl  8487  rankc2  8617  rankxpl  8621  rankxpsuc  8628  acnlem  8754  dfac2a  8835  fin23lem14  9038  fin23lem16  9040  fin23lem17  9043  fin23lem38  9054  fin23lem39  9055  itunisuc  9124  axdc3lem2  9156  axcclem  9162  ac5b  9183  ttukey  9223  wunex2  9439  wuncval2  9448  intgru  9515  pnfxr  9971  prdsval  15938  prdsds  15947  wunfunc  16382  wunnat  16439  arwval  16516  catcfuccl  16582  catcxpccl  16670  zrhval  19675  mreclatdemoBAD  20710  ptbasin2  21191  ptbasfi  21194  dfac14  21231  ptcmplem2  21667  ptcmplem3  21668  ptcmp  21672  cnextfvval  21679  cnextcn  21681  minveclem4a  23009  xrge0tsmsbi  29117  locfinreflem  29235  pstmfval  29267  pstmxmet  29268  esumex  29418  msrval  30689  dfrdg2  30945  trpredex  30981  fvbigcup  31179  ptrest  32578  heiborlem1  32780  heiborlem3  32782  heibor  32790  dicval  35483  aomclem1  36642  dfac21  36654  ntrrn  37440  ntrf  37441  dssmapntrcls  37446  fourierdlem70  39069  caragendifcl  39404  cnfsmf  39627  setrec1lem3  42235  setrec2fun  42238
  Copyright terms: Public domain W3C validator