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  kur14  23158  ispcon  23165  cvmscbv  23200  cvmsi  23207  cvmsval  23208  relexp0  23436  relexpsucr  23437  dfrdg2  23563  brbigcup  23849  dfbigcup2  23850  fobigcup  23851  brapply  23888  dfrdg4  23899  ordtoplem  24285  onsucsuccmpi  24293  limsucncmpi  24295  ordcmp  24297  isprsr  24636  ubos  24668  mxlelt  24676  mnlelt2  24678  isdir2  24704  qusp  24954  usptoplem  24958  istopx  24959  usptop  24962  prcnt  24963  islimrs  24992  bwt2  25004  isfne  25680  isref  25691  fneval  25699  isptfin  25707  islocfin  25708  comppfsc  25719  fnemeet1  25727  fnemeet2  25728  fnejoin1  25729  fnejoin2  25730  tailfval  25733  cover2  25770  cover2g  25771  istotbnd3  25907  sstotbnd  25911  heiborlem1  25947  heiborlem6  25952  heiborlem8  25954  isnacs3  26197  nacsfix  26199  stoweidlem35  27196  stoweidlem39  27200  stoweidlem50  27211  stoweidlem57  27218  csbfv12gALTVD  28048
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