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

Theorem unieq 3837
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 )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem unieq
StepHypRef Expression
1 rexeq 2738 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2398 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 3830 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 3830 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2341 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624    e. wcel 1685   {cab 2270   E.wrex 2545   U.cuni 3828
This theorem is referenced by:  unieqi  3838  unieqd  3839  uniintsn  3900  iununi  3987  treq  4120  limeq  4403  unizlim  4508  uniex  4515  uniexg  4516  onsucuni2  4624  onuninsuci  4630  orduninsuc  4633  elvvuni  4749  unielrel  5195  unixp0  5204  unixpid  5205  fvex  5499  opabiotafun  6284  undefval  6296  en1b  6924  nnunifi  7103  fissuni  7155  infeq5i  7332  infeq5  7333  trcl  7405  rankuni  7530  rankxplim3  7546  iunfictbso  7736  cflim2  7884  cfss  7886  cfslb  7887  fin2i  7916  fin1a2lem10  8030  fin1a2lem11  8031  fin1a2lem12  8032  itunisuc  8040  ituniiun  8043  hsmex  8053  dominf  8066  zornn0g  8127  dominfac  8190  wununi  8323  wunex2  8355  wuncval2  8364  incexclem  12289  mrcfval  13504  mrisval  13526  acsdrsel  14264  isacs4lem  14265  isacs5lem  14266  acsdrscl  14267  isps  14305  spwval2  14327  isdir  14348  sylow2a  14924  uniopn  16637  eltopspOLD  16650  istpsOLD  16652  istopon  16657  eltg3  16694  tgdom  16710  indistopon  16732  cldval  16754  ntrfval  16755  clsfval  16756  mretopd  16823  neifval  16830  lpfval  16864  isperf  16876  tgrest  16884  ist0  17042  ist1  17043  ishaus  17044  iscnrm  17045  iscmp  17109  cmpcov  17110  cmpcovf  17112  cncmp  17113  fincmp  17114  cmpsublem  17120  cmpsub  17121  tgcmp  17122  cmpcld  17123  uncmp  17124  hauscmplem  17127  cmpfi  17129  iscon  17133  is1stc  17161  2ndc1stc  17171  2ndcsep  17179  kgenval  17224  1stckgenlem  17242  txcmplem1  17329  txcmplem2  17330  kqval  17411  flffval  17678  fclsval  17697  fcfval  17722  alexsublem  17732  alexsubb  17734  alexsubALTlem2  17736  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  ptcmplem2  17741  ptcmplem3  17742  ptcmplem5  17744  icccmplem1  18321  icccmplem2  18322  bndth  18450  lebnumlem3  18455  om1val  18522  pi1val  18529  ovolicc2  18875  isplig  20836  hsupval  21905  kur14  23151  ispcon  23158  cvmscbv  23193  cvmsi  23200  cvmsval  23201  relexp0  23429  relexpsucr  23430  dfrdg2  23553  brbigcup  23846  dfbigcup2  23847  fobigcup  23848  brapply  23884  dfrdg4  23895  ordtoplem  24281  onsucsuccmpi  24289  limsucncmpi  24291  ordcmp  24293  isprsr  24623  ubos  24655  mxlelt  24663  mnlelt2  24665  isdir2  24691  qusp  24941  usptoplem  24945  istopx  24946  usptop  24949  prcnt  24950  islimrs  24979  bwt2  24991  isfne  25667  isref  25678  fneval  25686  isptfin  25694  islocfin  25695  comppfsc  25706  fnemeet1  25714  fnemeet2  25715  fnejoin1  25716  fnejoin2  25717  tailfval  25720  cover2  25757  cover2g  25758  istotbnd3  25894  sstotbnd  25898  heiborlem1  25934  heiborlem6  25939  heiborlem8  25941  isnacs3  26184  nacsfix  26186  stoweidlem35  27183  stoweidlem39  27187  stoweidlem50  27198  stoweidlem57  27205  csbfv12gALTVD  27943
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rex 2550  df-uni 3829
  Copyright terms: Public domain W3C validator