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

Theorem uniex 7285
 Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3427), 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 4721 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
32eleq1d 2850 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
4 uniex2 7284 . . 3 𝑦 𝑦 = 𝑥
54issetri 3431 . 2 𝑥 ∈ V
61, 3, 5vtocl 3478 1 𝐴 ∈ V
 Colors of variables: wff setvar class Syntax hints:   = wceq 1507   ∈ wcel 2050  Vcvv 3415  ∪ cuni 4713 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061  ax-un 7281 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rex 3094  df-v 3417  df-uni 4714 This theorem is referenced by:  vuniex  7286  unex  7288  iunpw  7311  elxp4  7444  elxp5  7445  1stval  7505  2ndval  7506  fo1st  7523  fo2nd  7524  cnvf1o  7616  brtpos2  7703  ixpsnf1o  8301  dffi3  8692  cnfcom2  8961  cnfcom3lem  8962  cnfcom3  8963  trcl  8966  rankc2  9096  rankxpl  9100  rankxpsuc  9107  acnlem  9270  dfac2a  9351  fin23lem14  9555  fin23lem16  9557  fin23lem17  9560  fin23lem38  9571  fin23lem39  9572  itunisuc  9641  axdc3lem2  9673  axcclem  9679  ac5b  9700  ttukey  9740  wunex2  9960  wuncval2  9969  intgru  10036  pnfex  10495  prdsval  16587  prdsds  16596  wunfunc  17030  wunnat  17087  arwval  17164  catcfuccl  17230  catcxpccl  17318  zrhval  20360  mreclatdemoBAD  21411  ptbasin2  21893  ptbasfi  21896  dfac14  21933  ptcmplem2  22368  ptcmplem3  22369  ptcmp  22373  cnextfvval  22380  cnextcn  22382  minveclem4a  23739  xrge0tsmsbi  30531  dimval  30630  dimvalfi  30631  locfinreflem  30748  pstmfval  30780  pstmxmet  30781  esumex  30932  msrval  32305  dfrdg2  32561  trpredex  32597  fvbigcup  32884  ctbssinf  34128  ptrest  34332  heiborlem1  34531  heiborlem3  34533  heibor  34541  dicval  37757  aomclem1  39050  dfac21  39062  ntrrn  39835  ntrf  39836  dssmapntrcls  39841  fourierdlem70  41893  caragendifcl  42228  cnfsmf  42449  setrec1lem3  44160  setrec2fun  44163
 Copyright terms: Public domain W3C validator