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

Theorem unieq 4026
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 2907 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2552 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 4019 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 4019 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2495 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   {cab 2424   E.wrex 2708   U.cuni 4017
This theorem is referenced by:  unieqi  4027  unieqd  4028  uniintsn  4089  iununi  4177  treq  4310  limeq  4595  unizlim  4700  uniex  4707  uniexg  4708  onsucuni2  4816  onuninsuci  4822  orduninsuc  4825  elvvuni  4940  unielrel  5396  unixp0  5405  unixpid  5406  opabiotafun  6538  undefval  6548  en1b  7177  nnunifi  7360  fissuni  7413  infeq5i  7593  infeq5  7594  trcl  7666  rankuni  7791  rankxplim3  7807  iunfictbso  7997  cflim2  8145  cfss  8147  cfslb  8148  fin2i  8177  fin1a2lem10  8291  fin1a2lem11  8292  fin1a2lem12  8293  itunisuc  8301  ituniiun  8304  hsmex  8314  dominf  8327  zornn0g  8387  dominfac  8450  wununi  8583  wunex2  8615  wuncval2  8624  incexclem  12618  mrcfval  13835  mrisval  13857  acsdrsel  14595  isacs4lem  14596  isacs5lem  14597  acsdrscl  14598  isps  14636  spwval2  14658  isdir  14679  sylow2a  15255  uniopn  16972  eltopspOLD  16985  istpsOLD  16987  istopon  16992  eltg3  17029  tgdom  17045  indistopon  17067  cldval  17089  ntrfval  17090  clsfval  17091  mretopd  17158  neifval  17165  lpfval  17204  isperf  17217  tgrest  17225  ist0  17386  ist1  17387  ishaus  17388  iscnrm  17389  iscmp  17453  cmpcov  17454  cmpcovf  17456  cncmp  17457  fincmp  17458  cmpsublem  17464  cmpsub  17465  tgcmp  17466  cmpcld  17467  uncmp  17468  hauscmplem  17471  cmpfi  17473  bwth  17475  iscon  17478  is1stc  17506  2ndc1stc  17516  2ndcsep  17524  kgenval  17569  1stckgenlem  17587  txcmplem1  17675  txcmplem2  17676  kqval  17760  flffval  18023  fclsval  18042  fcfval  18067  alexsublem  18077  alexsubb  18079  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  ptcmplem2  18086  ptcmplem3  18087  ptcmplem5  18089  cnextval  18094  iscfilu  18320  icccmplem1  18855  icccmplem2  18856  bndth  18985  lebnumlem3  18990  om1val  19057  pi1val  19064  ovolicc2  19420  isplig  21767  hsupval  22838  sigaclcu  24502  prsiga  24516  sigaclci  24517  unelsiga  24519  sigagenval  24525  measvun  24565  ismbfm  24604  isanmbfm  24608  dya2iocuni  24635  kur14  24904  ispcon  24912  cvmscbv  24947  cvmsi  24954  cvmsval  24955  relexp0  25131  relexpsucr  25132  dfrdg2  25425  brbigcup  25745  dfbigcup2  25746  fobigcup  25747  brapply  25785  dfrdg4  25797  ordtoplem  26187  onsucsuccmpi  26195  limsucncmpi  26197  ordcmp  26199  ovoliunnfl  26250  voliunnfl  26252  volsupnfl  26253  mbfresfi  26255  isfne  26350  isref  26361  fneval  26369  isptfin  26377  islocfin  26378  comppfsc  26389  fnemeet1  26397  fnemeet2  26398  fnejoin1  26399  fnejoin2  26400  tailfval  26403  cover2  26417  cover2g  26418  istotbnd3  26482  sstotbnd  26486  heiborlem1  26522  heiborlem6  26527  heiborlem8  26529  isnacs3  26766  nacsfix  26768  stoweidlem35  27762  stoweidlem39  27766  stoweidlem50  27777  stoweidlem57  27784  csbfv12gALTVD  29073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-uni 4018
  Copyright terms: Public domain W3C validator