MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unieq Unicode version

Theorem unieq 3736
Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
unieq  |-  ( A  =  B  ->  U. A  =  U. B )

Proof of Theorem unieq
StepHypRef Expression
1 rexeq 2690 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2363 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 3729 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 3729 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2310 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   {cab 2239   E.wrex 2510   U.cuni 3727
This theorem is referenced by:  unieqi  3737  unieqd  3738  uniintsn  3797  iununi  3884  treq  4016  limeq  4297  unizlim  4400  uniex  4407  uniexg  4408  onsucuni2  4516  onuninsuci  4522  orduninsuc  4525  elvvuni  4657  unielrel  5103  unixp0  5112  unixpid  5113  fvex  5391  opabiotafun  6175  undefval  6187  en1b  6814  nnunifi  6993  fissuni  7044  infeq5i  7221  infeq5  7222  trcl  7294  rankuni  7419  rankxplim3  7435  iunfictbso  7625  cflim2  7773  cfss  7775  cfslb  7776  fin2i  7805  fin1a2lem10  7919  fin1a2lem11  7920  fin1a2lem12  7921  itunisuc  7929  ituniiun  7932  hsmex  7942  dominf  7955  zornn0g  8016  dominfac  8075  wununi  8208  wunex2  8240  wuncval2  8249  mrcfval  13382  acsdrsel  14114  isacs4lem  14115  isacs5lem  14116  acsdrscl  14117  isps  14146  spwval2  14168  isdir  14189  sylow2a  14765  uniopn  16475  eltopspOLD  16488  istpsOLD  16490  istopon  16495  eltg3  16532  tgdom  16548  indistopon  16570  cldval  16592  ntrfval  16593  clsfval  16594  mretopd  16661  neifval  16668  lpfval  16702  isperf  16714  tgrest  16722  ist0  16880  ist1  16881  ishaus  16882  iscnrm  16883  iscmp  16947  cmpcov  16948  cmpcovf  16950  cncmp  16951  fincmp  16952  cmpsublem  16958  cmpsub  16959  tgcmp  16960  cmpcld  16961  uncmp  16962  hauscmplem  16965  cmpfi  16967  iscon  16971  is1stc  16999  2ndc1stc  17009  2ndcsep  17017  kgenval  17062  1stckgenlem  17080  txcmplem1  17167  txcmplem2  17168  kqval  17249  flffval  17516  fclsval  17535  fcfval  17560  alexsublem  17570  alexsubb  17572  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  ptcmplem2  17579  ptcmplem3  17580  ptcmplem5  17582  icccmplem1  18159  icccmplem2  18160  bndth  18288  lebnumlem3  18293  om1val  18360  pi1val  18367  ovolicc2  18713  isplig  20674  hsupval  21743  kur14  22918  ispcon  22925  cvmscbv  22960  cvmsi  22967  cvmsval  22968  relexp0  23196  relexpsucr  23197  dfrdg2  23320  brbigcup  23613  dfbigcup2  23614  fobigcup  23615  brapply  23651  dfrdg4  23662  ordtoplem  24048  onsucsuccmpi  24056  limsucncmpi  24058  ordcmp  24060  isprsr  24390  ubos  24422  mxlelt  24430  mnlelt2  24432  isdir2  24458  qusp  24708  usptoplem  24712  istopx  24713  usptop  24716  prcnt  24717  islimrs  24746  bwt2  24758  isfne  25434  isref  25445  fneval  25453  isptfin  25461  islocfin  25462  comppfsc  25473  fnemeet1  25481  fnemeet2  25482  fnejoin1  25483  fnejoin2  25484  tailfval  25487  cover2  25524  cover2g  25525  istotbnd3  25661  sstotbnd  25665  heiborlem1  25701  heiborlem6  25706  heiborlem8  25708  isnacs3  25951  nacsfix  25953  stoweidlem35  26918  stoweidlem39  26922  stoweidlem50  26933  stoweidlem57  26940  csbfv12gALTVD  27462
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-uni 3728
  Copyright terms: Public domain W3C validator