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

Theorem uniex 6824
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3175), 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 4370 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
32eleq1d 2667 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
4 uniex2 6823 . . 3 𝑦 𝑦 = 𝑥
54issetri 3178 . 2 𝑥 ∈ V
61, 3, 5vtocl 3227 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1975  Vcvv 3168   cuni 4362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-v 3170  df-uni 4363
This theorem is referenced by:  vuniex  6825  unex  6827  iunpw  6843  elxp4  6976  elxp5  6977  1stval  7034  2ndval  7035  fo1st  7052  fo2nd  7053  cnvf1o  7136  brtpos2  7218  ixpsnf1o  7807  dffi3  8193  cnfcom2  8455  cnfcom3lem  8456  cnfcom3  8457  trcl  8460  rankc2  8590  rankxpl  8594  rankxpsuc  8601  acnlem  8727  dfac2a  8808  fin23lem14  9011  fin23lem16  9013  fin23lem17  9016  fin23lem38  9027  fin23lem39  9028  itunisuc  9097  axdc3lem2  9129  axcclem  9135  ac5b  9156  ttukey  9196  wunex2  9412  wuncval2  9421  intgru  9488  pnfxr  11777  prdsval  15880  prdsds  15889  wunfunc  16324  wunnat  16381  arwval  16458  catcfuccl  16524  catcxpccl  16612  zrhval  19616  mreclatdemoBAD  20648  ptbasin2  21129  ptbasfi  21132  dfac14  21169  ptcmplem2  21605  ptcmplem3  21606  ptcmp  21610  cnextfvval  21617  cnextcn  21619  minveclem4a  22922  xrge0tsmsbi  28919  locfinreflem  29037  pstmfval  29069  pstmxmet  29070  esumex  29220  msrval  30491  dfrdg2  30747  trpredex  30783  fvbigcup  30981  ptrest  32377  heiborlem1  32579  heiborlem3  32581  heibor  32589  dicval  35282  aomclem1  36441  dfac21  36453  ntrrn  37239  ntrf  37240  dssmapntrcls  37245  fourierdlem70  38869  caragendifcl  39204  cnfsmf  39427
  Copyright terms: Public domain W3C validator