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

Theorem unieq 4257
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

Proof of Theorem unieq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexeq 3055 . . 3
21abbidv 2593 . 2
3 dfuni2 4251 . 2
4 dfuni2 4251 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {cab 2442  E.wrex 2808  U.cuni 4249
This theorem is referenced by:  unieqi  4258  unieqd  4259  uniintsn  4324  iununi  4415  treq  4551  limeq  4895  unizlim  4999  elvvuni  5065  unielrel  5537  unixp0  5546  unixpid  5547  opabiotafun  5934  uniex  6596  uniexg  6597  onsucuni2  6669  onuninsuci  6675  orduninsuc  6678  undefval  7024  en1b  7603  nnunifi  7791  fissuni  7845  infeq5i  8074  infeq5  8075  trcl  8180  rankuni  8302  rankxplim3  8320  iunfictbso  8516  cflim2  8664  cfss  8666  cfslb  8667  fin2i  8696  fin1a2lem10  8810  fin1a2lem11  8811  fin1a2lem12  8812  itunisuc  8820  ituniiun  8823  hsmex  8833  dominf  8846  zornn0g  8906  dominfac  8969  wununi  9105  wunex2  9137  wuncval2  9146  incexclem  13648  mrcfval  15005  mrisval  15027  acsdrsel  15797  isacs4lem  15798  isacs5lem  15799  acsdrscl  15800  isps  15832  isdir  15862  sylow2a  16639  uniopn  19406  eltopspOLD  19419  istpsOLD  19421  istopon  19426  eltg3  19463  tgdom  19480  indistopon  19502  cldval  19524  ntrfval  19525  clsfval  19526  mretopd  19593  neifval  19600  lpfval  19639  isperf  19652  tgrest  19660  ist0  19821  ist1  19822  ishaus  19823  iscnrm  19824  iscmp  19888  cmpcov  19889  cmpcovf  19891  cncmp  19892  fincmp  19893  cmpsublem  19899  cmpsub  19900  tgcmp  19901  cmpcld  19902  uncmp  19903  hauscmplem  19906  cmpfi  19908  bwthOLD  19911  iscon  19914  is1stc  19942  2ndc1stc  19952  2ndcsep  19960  isref  20010  isptfin  20017  islocfin  20018  comppfsc  20033  kgenval  20036  1stckgenlem  20054  txcmplem1  20142  txcmplem2  20143  kqval  20227  flffval  20490  fclsval  20509  fcfval  20534  alexsublem  20544  alexsubb  20546  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem2  20553  ptcmplem3  20554  ptcmplem5  20556  cnextval  20561  iscfilu  20791  icccmplem1  21327  icccmplem2  21328  bndth  21458  lebnumlem3  21463  om1val  21530  pi1val  21537  ovolicc2  21933  isplig  25179  hsupval  26252  iscref  27847  crefi  27850  cmpcref  27853  pcmplfin  27863  sigaclcu  28117  prsiga  28131  sigaclci  28132  unelsiga  28134  sigagenval  28140  measvun  28180  ismbfm  28223  isanmbfm  28227  dya2iocuni  28254  oms0  28266  kur14  28660  ispcon  28668  cvmscbv  28703  cvmsi  28710  cvmsval  28711  relexp0  29052  relexpsucr  29053  dfrdg2  29228  brbigcup  29548  dfbigcup2  29549  fobigcup  29550  brapply  29588  dfrdg4  29600  ordtoplem  29900  onsucsuccmpi  29908  limsucncmpi  29910  ordcmp  29912  heicant  30049  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  mbfresfi  30061  isfne  30157  fneval  30170  fnemeet1  30184  fnemeet2  30185  fnejoin1  30186  fnejoin2  30187  tailfval  30190  cover2  30204  cover2g  30205  istotbnd3  30267  sstotbnd  30271  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  isnacs3  30642  nacsfix  30644  stoweidlem35  31817  stoweidlem39  31821  stoweidlem50  31832  stoweidlem57  31839  csbfv12gALTVD  33699  pwelg  37745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250
  Copyright terms: Public domain W3C validator