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

Theorem unieq 4016
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 2897 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2549 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 4009 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 4009 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2492 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {cab 2421   E.wrex 2698   U.cuni 4007
This theorem is referenced by:  unieqi  4017  unieqd  4018  uniintsn  4079  iununi  4167  treq  4300  limeq  4585  unizlim  4689  uniex  4696  uniexg  4697  onsucuni2  4805  onuninsuci  4811  orduninsuc  4814  elvvuni  4929  unielrel  5385  unixp0  5394  unixpid  5395  opabiotafun  6527  undefval  6537  en1b  7166  nnunifi  7349  fissuni  7402  infeq5i  7580  infeq5  7581  trcl  7653  rankuni  7778  rankxplim3  7794  iunfictbso  7984  cflim2  8132  cfss  8134  cfslb  8135  fin2i  8164  fin1a2lem10  8278  fin1a2lem11  8279  fin1a2lem12  8280  itunisuc  8288  ituniiun  8291  hsmex  8301  dominf  8314  zornn0g  8374  dominfac  8437  wununi  8570  wunex2  8602  wuncval2  8611  incexclem  12604  mrcfval  13821  mrisval  13843  acsdrsel  14581  isacs4lem  14582  isacs5lem  14583  acsdrscl  14584  isps  14622  spwval2  14644  isdir  14665  sylow2a  15241  uniopn  16958  eltopspOLD  16971  istpsOLD  16973  istopon  16978  eltg3  17015  tgdom  17031  indistopon  17053  cldval  17075  ntrfval  17076  clsfval  17077  mretopd  17144  neifval  17151  lpfval  17190  isperf  17203  tgrest  17211  ist0  17372  ist1  17373  ishaus  17374  iscnrm  17375  iscmp  17439  cmpcov  17440  cmpcovf  17442  cncmp  17443  fincmp  17444  cmpsublem  17450  cmpsub  17451  tgcmp  17452  cmpcld  17453  uncmp  17454  hauscmplem  17457  cmpfi  17459  bwth  17461  iscon  17464  is1stc  17492  2ndc1stc  17502  2ndcsep  17510  kgenval  17555  1stckgenlem  17573  txcmplem1  17661  txcmplem2  17662  kqval  17746  flffval  18009  fclsval  18028  fcfval  18053  alexsublem  18063  alexsubb  18065  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  ptcmplem2  18072  ptcmplem3  18073  ptcmplem5  18075  cnextval  18080  iscfilu  18306  icccmplem1  18841  icccmplem2  18842  bndth  18971  lebnumlem3  18976  om1val  19043  pi1val  19050  ovolicc2  19406  isplig  21753  hsupval  22824  sigaclcu  24488  prsiga  24502  sigaclci  24503  unelsiga  24505  sigagenval  24511  measvun  24551  ismbfm  24590  isanmbfm  24594  dya2iocuni  24621  kur14  24890  ispcon  24898  cvmscbv  24933  cvmsi  24940  cvmsval  24941  relexp0  25117  relexpsucr  25118  dfrdg2  25407  brbigcup  25693  dfbigcup2  25694  fobigcup  25695  brapply  25733  dfrdg4  25745  ordtoplem  26133  onsucsuccmpi  26141  limsucncmpi  26143  ordcmp  26145  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  mbfresfi  26199  isfne  26285  isref  26296  fneval  26304  isptfin  26312  islocfin  26313  comppfsc  26324  fnemeet1  26332  fnemeet2  26333  fnejoin1  26334  fnejoin2  26335  tailfval  26338  cover2  26352  cover2g  26353  istotbnd3  26417  sstotbnd  26421  heiborlem1  26457  heiborlem6  26462  heiborlem8  26464  isnacs3  26701  nacsfix  26703  stoweidlem35  27698  stoweidlem39  27702  stoweidlem50  27713  stoweidlem57  27720  csbfv12gALTVD  28865
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-uni 4008
  Copyright terms: Public domain W3C validator