Theorem unieq 4199

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.

Step	Hyp	Ref	Expression
1		rexeq 3005	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2538	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4193	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4193	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2468	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1405   {cab 2387   E.wrex 2755   U.cuni 4191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760  df-uni 4192

This theorem is referenced by:  unieqi  4200  unieqd  4201  uniintsn  4265  iununi  4359  treq  4495  elvvuni  4884  unielrel  5348  unixp0  5358  unixpid  5359  limeq  5422  unizlim  5526  opabiotafun  5910  uniex  6578  uniexg  6579  onsucuni2  6652  onuninsuci  6658  orduninsuc  6661  undefval  7008  en1b  7621  nnunifi  7805  fissuni  7859  infeq5i  8086  infeq5  8087  trcl  8191  rankuni  8313  rankxplim3  8331  iunfictbso  8527  cflim2  8675  cfss  8677  cfslb  8678  fin2i  8707  fin1a2lem10  8821  fin1a2lem11  8822  fin1a2lem12  8823  itunisuc  8831  ituniiun  8834  hsmex  8844  dominf  8857  zornn0g  8917  dominfac  8980  wununi  9114  wunex2  9146  wuncval2  9155  incexclem  13799  mrcfval  15222  mrisval  15244  acsdrsel  16121  isacs4lem  16122  isacs5lem  16123  acsdrscl  16124  isps  16156  isdir  16186  sylow2a  16963  uniopn  19698  eltopspOLD  19711  istpsOLD  19713  istopon  19718  eltg3  19755  tgdom  19772  indistopon  19794  cldval  19816  ntrfval  19817  clsfval  19818  mretopd  19886  neifval  19893  lpfval  19932  isperf  19945  tgrest  19953  ist0  20114  ist1  20115  ishaus  20116  iscnrm  20117  iscmp  20181  cmpcov  20182  cmpcovf  20184  cncmp  20185  fincmp  20186  cmpsublem  20192  cmpsub  20193  tgcmp  20194  cmpcld  20195  uncmp  20196  hauscmplem  20199  cmpfi  20201  iscon  20206  is1stc  20234  2ndc1stc  20244  2ndcsep  20252  isref  20302  isptfin  20309  islocfin  20310  comppfsc  20325  kgenval  20328  1stckgenlem  20346  txcmplem1  20434  txcmplem2  20435  kqval  20519  flffval  20782  fclsval  20801  fcfval  20826  alexsublem  20836  alexsubb  20838  alexsubALTlem2  20840  alexsubALTlem3  20841  alexsubALTlem4  20842  alexsubALT  20843  ptcmplem2  20845  ptcmplem3  20846  ptcmplem5  20848  cnextval  20853  iscfilu  21083  icccmplem1  21619  icccmplem2  21620  bndth  21750  lebnumlem3  21755  om1val  21822  pi1val  21829  ovolicc2  22225  isplig  25597  hsupval  26666  acunirnmpt  27943  iscref  28300  crefi  28303  cmpcref  28306  pcmplfin  28316  sigaclcu  28565  prsiga  28579  sigaclci  28580  unelsiga  28582  sigagenval  28588  unelldsys  28606  sigapildsys  28610  ldgenpisyslem1  28611  rossros  28628  measvun  28657  ismbfm  28700  isanmbfm  28704  dya2iocuni  28731  oms0  28745  omssubadd  28748  carsgsigalem  28763  fiunelcarsg  28764  carsgclctunlem1  28765  carsgclctunlem2  28767  carsgclctunlem3  28768  carsgclctun  28769  pmeasmono  28772  pmeasadd  28773  kur14  29513  ispcon  29520  cvmscbv  29555  cvmsi  29562  cvmsval  29563  dfrdg2  30015  brbigcup  30236  dfbigcup2  30237  fobigcup  30238  brapply  30276  dfrdg4  30289  isfne  30567  fneval  30580  fnemeet1  30594  fnemeet2  30595  fnejoin1  30596  fnejoin2  30597  tailfval  30600  ordtoplem  30667  onsucsuccmpi  30675  limsucncmpi  30677  ordcmp  30679  dissneqlem  31256  heicant  31421  ovoliunnfl  31428  voliunnfl  31430  volsupnfl  31431  mbfresfi  31433  cover2  31486  cover2g  31487  istotbnd3  31549  sstotbnd  31553  heiborlem1  31589  heiborlem6  31594  heiborlem8  31596  isnacs3  35004  nacsfix  35006  pwelg  35611  csbfv12gALTVD  36730  stoweidlem35  37185  stoweidlem39  37189  stoweidlem50  37200  stoweidlem57  37207