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

Theorem uniex 6938
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3202), 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 4435 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
32eleq1d 2684 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
4 uniex2 6937 . . 3 𝑦 𝑦 = 𝑥
54issetri 3205 . 2 𝑥 ∈ V
61, 3, 5vtocl 3254 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wcel 1988  Vcvv 3195   cuni 4427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-v 3197  df-uni 4428
This theorem is referenced by:  vuniex  6939  unex  6941  iunpw  6963  elxp4  7095  elxp5  7096  1stval  7155  2ndval  7156  fo1st  7173  fo2nd  7174  cnvf1o  7261  brtpos2  7343  ixpsnf1o  7933  dffi3  8322  cnfcom2  8584  cnfcom3lem  8585  cnfcom3  8586  trcl  8589  rankc2  8719  rankxpl  8723  rankxpsuc  8730  acnlem  8856  dfac2a  8937  fin23lem14  9140  fin23lem16  9142  fin23lem17  9145  fin23lem38  9156  fin23lem39  9157  itunisuc  9226  axdc3lem2  9258  axcclem  9264  ac5b  9285  ttukey  9325  wunex2  9545  wuncval2  9554  intgru  9621  pnfxr  10077  prdsval  16096  prdsds  16105  wunfunc  16540  wunnat  16597  arwval  16674  catcfuccl  16740  catcxpccl  16828  zrhval  19837  mreclatdemoBAD  20881  ptbasin2  21362  ptbasfi  21365  dfac14  21402  ptcmplem2  21838  ptcmplem3  21839  ptcmp  21843  cnextfvval  21850  cnextcn  21852  minveclem4a  23182  xrge0tsmsbi  29760  locfinreflem  29881  pstmfval  29913  pstmxmet  29914  esumex  30065  msrval  31409  dfrdg2  31675  trpredex  31711  fvbigcup  31984  ptrest  33379  heiborlem1  33581  heiborlem3  33583  heibor  33591  dicval  36284  aomclem1  37443  dfac21  37455  ntrrn  38240  ntrf  38241  dssmapntrcls  38246  fourierdlem70  40156  caragendifcl  40491  cnfsmf  40712  setrec1lem3  42201  setrec2fun  42204
  Copyright terms: Public domain W3C validator