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

Theorem unieq 4224
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexeq 3026 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2558 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 4218 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 4218 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2488 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   {cab 2407   E.wrex 2776   U.cuni 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rex 2781  df-uni 4217
This theorem is referenced by:  unieqi  4225  unieqd  4226  uniintsn  4290  iununi  4384  treq  4521  elvvuni  4911  unielrel  5376  unixp0  5386  unixpid  5387  limeq  5451  unizlim  5555  opabiotafun  5939  uniex  6598  uniexg  6599  onsucuni2  6672  onuninsuci  6678  orduninsuc  6681  undefval  7028  en1b  7641  nnunifi  7825  fissuni  7882  infeq5i  8144  infeq5  8145  trcl  8214  rankuni  8336  rankxplim3  8354  iunfictbso  8546  cflim2  8694  cfss  8696  cfslb  8697  fin2i  8726  fin1a2lem10  8840  fin1a2lem11  8841  fin1a2lem12  8842  itunisuc  8850  ituniiun  8853  hsmex  8863  dominf  8876  zornn0g  8936  dominfac  8999  wununi  9132  wunex2  9164  wuncval2  9173  incexclem  13882  mrcfval  15502  mrisval  15524  acsdrsel  16401  isacs4lem  16402  isacs5lem  16403  acsdrscl  16404  isps  16436  isdir  16466  sylow2a  17259  uniopn  19914  istopon  19927  eltg3  19964  tgdom  19981  indistopon  20003  cldval  20025  ntrfval  20026  clsfval  20027  mretopd  20095  neifval  20102  lpfval  20141  isperf  20154  tgrest  20162  ist0  20323  ist1  20324  ishaus  20325  iscnrm  20326  iscmp  20390  cmpcov  20391  cmpcovf  20393  cncmp  20394  fincmp  20395  cmpsublem  20401  cmpsub  20402  tgcmp  20403  cmpcld  20404  uncmp  20405  hauscmplem  20408  cmpfi  20410  iscon  20415  is1stc  20443  2ndc1stc  20453  2ndcsep  20461  isref  20511  isptfin  20518  islocfin  20519  comppfsc  20534  kgenval  20537  1stckgenlem  20555  txcmplem1  20643  txcmplem2  20644  kqval  20728  flffval  20991  fclsval  21010  fcfval  21035  alexsublem  21046  alexsubb  21048  alexsubALTlem2  21050  alexsubALTlem3  21051  alexsubALTlem4  21052  alexsubALT  21053  ptcmplem2  21055  ptcmplem3  21056  ptcmplem5  21058  cnextval  21063  iscfilu  21290  icccmplem1  21827  icccmplem2  21828  bndth  21973  lebnumlem3  21978  lebnumlem3OLD  21981  om1val  22048  pi1val  22055  ovolicc2  22463  isplig  25895  hsupval  26973  acunirnmpt  28251  iscref  28667  crefi  28670  cmpcref  28673  pcmplfin  28683  sigaclcu  28935  prsiga  28949  sigaclci  28950  unelsiga  28952  sigagenval  28958  unelldsys  28976  sigapildsys  28980  ldgenpisyslem1  28981  rossros  28998  measvun  29027  ismbfm  29070  isanmbfm  29074  dya2iocuni  29101  oms0  29121  omssubadd  29124  oms0OLD  29125  omssubaddOLD  29128  carsgsigalem  29143  fiunelcarsg  29144  carsgclctunlem1  29145  carsgclctunlem2  29147  carsgclctunlem3  29148  carsgclctun  29149  pmeasmono  29153  pmeasadd  29154  kur14  29935  ispcon  29942  cvmscbv  29977  cvmsi  29984  cvmsval  29985  dfrdg2  30437  brbigcup  30658  dfbigcup2  30659  fobigcup  30660  brapply  30698  dfrdg4  30711  isfne  30988  fneval  31001  fnemeet1  31015  fnemeet2  31016  fnejoin1  31017  fnejoin2  31018  tailfval  31021  ordtoplem  31088  onsucsuccmpi  31096  limsucncmpi  31098  ordcmp  31100  dissneqlem  31683  heicant  31889  ovoliunnfl  31896  voliunnfl  31898  volsupnfl  31899  mbfresfi  31901  cover2  31954  cover2g  31955  istotbnd3  32017  sstotbnd  32021  heiborlem1  32057  heiborlem6  32062  heiborlem8  32064  isnacs3  35471  nacsfix  35473  pwelg  36084  csbfv12gALTVD  37157  stoweidlem35  37716  stoweidlem39  37720  stoweidlem50  37731  stoweidlem57  37738  issal  37976  salunicl  37978  saluncl  37979  prsal  37980  salgenval  37983  intsaluni  37989  salgencl  37991  meadjuni  38074  ismeannd  38084  omeunile  38105  caragenunicl  38124  isomennd  38131
  Copyright terms: Public domain W3C validator