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

Theorem unieq 3852
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 2750 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2410 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 3845 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 3845 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   {cab 2282   E.wrex 2557   U.cuni 3843
This theorem is referenced by:  unieqi  3853  unieqd  3854  uniintsn  3915  iununi  4002  treq  4135  limeq  4420  unizlim  4525  uniex  4532  uniexg  4533  onsucuni2  4641  onuninsuci  4647  orduninsuc  4650  elvvuni  4766  unielrel  5213  unixp0  5222  unixpid  5223  opabiotafun  6307  undefval  6317  en1b  6945  nnunifi  7124  fissuni  7176  infeq5i  7353  infeq5  7354  trcl  7426  rankuni  7551  rankxplim3  7567  iunfictbso  7757  cflim2  7905  cfss  7907  cfslb  7908  fin2i  7937  fin1a2lem10  8051  fin1a2lem11  8052  fin1a2lem12  8053  itunisuc  8061  ituniiun  8064  hsmex  8074  dominf  8087  zornn0g  8148  dominfac  8211  wununi  8344  wunex2  8376  wuncval2  8385  incexclem  12311  mrcfval  13526  mrisval  13548  acsdrsel  14286  isacs4lem  14287  isacs5lem  14288  acsdrscl  14289  isps  14327  spwval2  14349  isdir  14370  sylow2a  14946  uniopn  16659  eltopspOLD  16672  istpsOLD  16674  istopon  16679  eltg3  16716  tgdom  16732  indistopon  16754  cldval  16776  ntrfval  16777  clsfval  16778  mretopd  16845  neifval  16852  lpfval  16886  isperf  16898  tgrest  16906  ist0  17064  ist1  17065  ishaus  17066  iscnrm  17067  iscmp  17131  cmpcov  17132  cmpcovf  17134  cncmp  17135  fincmp  17136  cmpsublem  17142  cmpsub  17143  tgcmp  17144  cmpcld  17145  uncmp  17146  hauscmplem  17149  cmpfi  17151  iscon  17155  is1stc  17183  2ndc1stc  17193  2ndcsep  17201  kgenval  17246  1stckgenlem  17264  txcmplem1  17351  txcmplem2  17352  kqval  17433  flffval  17700  fclsval  17719  fcfval  17744  alexsublem  17754  alexsubb  17756  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  ptcmplem5  17766  icccmplem1  18343  icccmplem2  18344  bndth  18472  lebnumlem3  18477  om1val  18544  pi1val  18551  ovolicc2  18897  isplig  20860  hsupval  21929  sigaclcu  23493  prsiga  23507  sigaclci  23508  unelsiga  23510  sigagenval  23516  measvun  23552  ismbfm  23572  isanmbfm  23576  kur14  23762  ispcon  23769  cvmscbv  23804  cvmsi  23811  cvmsval  23812  relexp0  24040  relexpsucr  24041  dfrdg2  24223  brbigcup  24509  dfbigcup2  24510  fobigcup  24511  brapply  24548  dfrdg4  24560  ordtoplem  24946  onsucsuccmpi  24954  limsucncmpi  24956  ordcmp  24958  ovoliunnfl  25001  isprsr  25327  ubos  25359  mxlelt  25367  mnlelt2  25369  isdir2  25395  qusp  25645  usptoplem  25649  istopx  25650  usptop  25653  prcnt  25654  islimrs  25683  bwt2  25695  isfne  26371  isref  26382  fneval  26390  isptfin  26398  islocfin  26399  comppfsc  26410  fnemeet1  26418  fnemeet2  26419  fnejoin1  26420  fnejoin2  26421  tailfval  26424  cover2  26461  cover2g  26462  istotbnd3  26598  sstotbnd  26602  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  isnacs3  26888  nacsfix  26890  stoweidlem35  27887  stoweidlem39  27891  stoweidlem50  27902  stoweidlem57  27909  csbfv12gALTVD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-uni 3844
  Copyright terms: Public domain W3C validator