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

Theorem unieq 3810
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
StepHypRef Expression
1 rexeq 2712 . . 3  |-  ( A  =  B  ->  ( E. x  e.  A  y  e.  x  <->  E. x  e.  B  y  e.  x ) )
21abbidv 2372 . 2  |-  ( A  =  B  ->  { y  |  E. x  e.  A  y  e.  x }  =  { y  |  E. x  e.  B  y  e.  x }
)
3 dfuni2 3803 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
4 dfuni2 3803 . 2  |-  U. B  =  { y  |  E. x  e.  B  y  e.  x }
52, 3, 43eqtr4g 2315 1  |-  ( A  =  B  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   {cab 2244   E.wrex 2519   U.cuni 3801
This theorem is referenced by:  unieqi  3811  unieqd  3812  uniintsn  3873  iununi  3960  treq  4093  limeq  4376  unizlim  4481  uniex  4488  uniexg  4489  onsucuni2  4597  onuninsuci  4603  orduninsuc  4606  elvvuni  4738  unielrel  5184  unixp0  5193  unixpid  5194  fvex  5472  opabiotafun  6257  undefval  6269  en1b  6897  nnunifi  7076  fissuni  7128  infeq5i  7305  infeq5  7306  trcl  7378  rankuni  7503  rankxplim3  7519  iunfictbso  7709  cflim2  7857  cfss  7859  cfslb  7860  fin2i  7889  fin1a2lem10  8003  fin1a2lem11  8004  fin1a2lem12  8005  itunisuc  8013  ituniiun  8016  hsmex  8026  dominf  8039  zornn0g  8100  dominfac  8163  wununi  8296  wunex2  8328  wuncval2  8337  mrcfval  13472  mrisval  13494  acsdrsel  14232  isacs4lem  14233  isacs5lem  14234  acsdrscl  14235  isps  14273  spwval2  14295  isdir  14316  sylow2a  14892  uniopn  16605  eltopspOLD  16618  istpsOLD  16620  istopon  16625  eltg3  16662  tgdom  16678  indistopon  16700  cldval  16722  ntrfval  16723  clsfval  16724  mretopd  16791  neifval  16798  lpfval  16832  isperf  16844  tgrest  16852  ist0  17010  ist1  17011  ishaus  17012  iscnrm  17013  iscmp  17077  cmpcov  17078  cmpcovf  17080  cncmp  17081  fincmp  17082  cmpsublem  17088  cmpsub  17089  tgcmp  17090  cmpcld  17091  uncmp  17092  hauscmplem  17095  cmpfi  17097  iscon  17101  is1stc  17129  2ndc1stc  17139  2ndcsep  17147  kgenval  17192  1stckgenlem  17210  txcmplem1  17297  txcmplem2  17298  kqval  17379  flffval  17646  fclsval  17665  fcfval  17690  alexsublem  17700  alexsubb  17702  alexsubALTlem2  17704  alexsubALTlem3  17705  alexsubALTlem4  17706  alexsubALT  17707  ptcmplem2  17709  ptcmplem3  17710  ptcmplem5  17712  icccmplem1  18289  icccmplem2  18290  bndth  18418  lebnumlem3  18423  om1val  18490  pi1val  18497  ovolicc2  18843  isplig  20804  hsupval  21873  kur14  23119  ispcon  23126  cvmscbv  23161  cvmsi  23168  cvmsval  23169  relexp0  23397  relexpsucr  23398  dfrdg2  23521  brbigcup  23814  dfbigcup2  23815  fobigcup  23816  brapply  23852  dfrdg4  23863  ordtoplem  24249  onsucsuccmpi  24257  limsucncmpi  24259  ordcmp  24261  isprsr  24591  ubos  24623  mxlelt  24631  mnlelt2  24633  isdir2  24659  qusp  24909  usptoplem  24913  istopx  24914  usptop  24917  prcnt  24918  islimrs  24947  bwt2  24959  isfne  25635  isref  25646  fneval  25654  isptfin  25662  islocfin  25663  comppfsc  25674  fnemeet1  25682  fnemeet2  25683  fnejoin1  25684  fnejoin2  25685  tailfval  25688  cover2  25725  cover2g  25726  istotbnd3  25862  sstotbnd  25866  heiborlem1  25902  heiborlem6  25907  heiborlem8  25909  isnacs3  26152  nacsfix  26154  stoweidlem35  27119  stoweidlem39  27123  stoweidlem50  27134  stoweidlem57  27141  csbfv12gALTVD  27725
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rex 2524  df-uni 3802
  Copyright terms: Public domain W3C validator