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

Theorem unieq 3836
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 2737 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2397 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 3829 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 3829 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {cab 2269   E.wrex 2544   U.cuni 3827
This theorem is referenced by:  unieqi  3837  unieqd  3838  uniintsn  3899  iununi  3986  treq  4119  limeq  4404  unizlim  4509  uniex  4516  uniexg  4517  onsucuni2  4625  onuninsuci  4631  orduninsuc  4634  elvvuni  4750  unielrel  5197  unixp0  5206  unixpid  5207  opabiotafun  6291  undefval  6301  en1b  6929  nnunifi  7108  fissuni  7160  infeq5i  7337  infeq5  7338  trcl  7410  rankuni  7535  rankxplim3  7551  iunfictbso  7741  cflim2  7889  cfss  7891  cfslb  7892  fin2i  7921  fin1a2lem10  8035  fin1a2lem11  8036  fin1a2lem12  8037  itunisuc  8045  ituniiun  8048  hsmex  8058  dominf  8071  zornn0g  8132  dominfac  8195  wununi  8328  wunex2  8360  wuncval2  8369  incexclem  12295  mrcfval  13510  mrisval  13532  acsdrsel  14270  isacs4lem  14271  isacs5lem  14272  acsdrscl  14273  isps  14311  spwval2  14333  isdir  14354  sylow2a  14930  uniopn  16643  eltopspOLD  16656  istpsOLD  16658  istopon  16663  eltg3  16700  tgdom  16716  indistopon  16738  cldval  16760  ntrfval  16761  clsfval  16762  mretopd  16829  neifval  16836  lpfval  16870  isperf  16882  tgrest  16890  ist0  17048  ist1  17049  ishaus  17050  iscnrm  17051  iscmp  17115  cmpcov  17116  cmpcovf  17118  cncmp  17119  fincmp  17120  cmpsublem  17126  cmpsub  17127  tgcmp  17128  cmpcld  17129  uncmp  17130  hauscmplem  17133  cmpfi  17135  iscon  17139  is1stc  17167  2ndc1stc  17177  2ndcsep  17185  kgenval  17230  1stckgenlem  17248  txcmplem1  17335  txcmplem2  17336  kqval  17417  flffval  17684  fclsval  17703  fcfval  17728  alexsublem  17738  alexsubb  17740  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  ptcmplem5  17750  icccmplem1  18327  icccmplem2  18328  bndth  18456  lebnumlem3  18461  om1val  18528  pi1val  18535  ovolicc2  18881  isplig  20844  hsupval  21913  sigaclcu  23478  prsiga  23492  sigaclci  23493  unelsiga  23495  sigagenval  23501  measvun  23537  ismbfm  23557  isanmbfm  23561  kur14  23747  ispcon  23754  cvmscbv  23789  cvmsi  23796  cvmsval  23797  relexp0  24025  relexpsucr  24026  dfrdg2  24152  brbigcup  24438  dfbigcup2  24439  fobigcup  24440  brapply  24477  dfrdg4  24488  ordtoplem  24874  onsucsuccmpi  24882  limsucncmpi  24884  ordcmp  24886  isprsr  25224  ubos  25256  mxlelt  25264  mnlelt2  25266  isdir2  25292  qusp  25542  usptoplem  25546  istopx  25547  usptop  25550  prcnt  25551  islimrs  25580  bwt2  25592  isfne  26268  isref  26279  fneval  26287  isptfin  26295  islocfin  26296  comppfsc  26307  fnemeet1  26315  fnemeet2  26316  fnejoin1  26317  fnejoin2  26318  tailfval  26321  cover2  26358  cover2g  26359  istotbnd3  26495  sstotbnd  26499  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  isnacs3  26785  nacsfix  26787  stoweidlem35  27784  stoweidlem39  27788  stoweidlem50  27799  stoweidlem57  27806  csbfv12gALTVD  28675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828
  Copyright terms: Public domain W3C validator