Theorem unieq 4259

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 3055	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2593	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4253	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4253	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2523	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1395   {cab 2442   E.wrex 2808   U.cuni 4251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4252

This theorem is referenced by:  unieqi  4260  unieqd  4261  uniintsn  4326  iununi  4420  treq  4556  limeq  4899  unizlim  5003  elvvuni  5069  unielrel  5538  unixp0  5547  unixpid  5548  opabiotafun  5934  uniex  6595  uniexg  6596  onsucuni2  6668  onuninsuci  6674  orduninsuc  6677  undefval  7023  en1b  7602  nnunifi  7789  fissuni  7843  infeq5i  8070  infeq5  8071  trcl  8176  rankuni  8298  rankxplim3  8316  iunfictbso  8512  cflim2  8660  cfss  8662  cfslb  8663  fin2i  8692  fin1a2lem10  8806  fin1a2lem11  8807  fin1a2lem12  8808  itunisuc  8816  ituniiun  8819  hsmex  8829  dominf  8842  zornn0g  8902  dominfac  8965  wununi  9101  wunex2  9133  wuncval2  9142  incexclem  13660  mrcfval  15025  mrisval  15047  acsdrsel  15924  isacs4lem  15925  isacs5lem  15926  acsdrscl  15927  isps  15959  isdir  15989  sylow2a  16766  uniopn  19533  eltopspOLD  19546  istpsOLD  19548  istopon  19553  eltg3  19590  tgdom  19607  indistopon  19629  cldval  19651  ntrfval  19652  clsfval  19653  mretopd  19720  neifval  19727  lpfval  19766  isperf  19779  tgrest  19787  ist0  19948  ist1  19949  ishaus  19950  iscnrm  19951  iscmp  20015  cmpcov  20016  cmpcovf  20018  cncmp  20019  fincmp  20020  cmpsublem  20026  cmpsub  20027  tgcmp  20028  cmpcld  20029  uncmp  20030  hauscmplem  20033  cmpfi  20035  iscon  20040  is1stc  20068  2ndc1stc  20078  2ndcsep  20086  isref  20136  isptfin  20143  islocfin  20144  comppfsc  20159  kgenval  20162  1stckgenlem  20180  txcmplem1  20268  txcmplem2  20269  kqval  20353  flffval  20616  fclsval  20635  fcfval  20660  alexsublem  20670  alexsubb  20672  alexsubALTlem2  20674  alexsubALTlem3  20675  alexsubALTlem4  20676  alexsubALT  20677  ptcmplem2  20679  ptcmplem3  20680  ptcmplem5  20682  cnextval  20687  iscfilu  20917  icccmplem1  21453  icccmplem2  21454  bndth  21584  lebnumlem3  21589  om1val  21656  pi1val  21663  ovolicc2  22059  isplig  25306  hsupval  26379  acunirnmpt  27653  iscref  28008  crefi  28011  cmpcref  28014  pcmplfin  28024  sigaclcu  28290  prsiga  28304  sigaclci  28305  unelsiga  28307  sigagenval  28313  measvun  28353  ismbfm  28396  isanmbfm  28400  dya2iocuni  28427  oms0  28441  omssubadd  28444  carsgsigalem  28458  fiunelcarsg  28459  carsgclctunlem1  28460  carsgclctunlem2  28461  carsgclctunlem3  28462  carsgclctun  28463  kur14  28857  ispcon  28865  cvmscbv  28900  cvmsi  28907  cvmsval  28908  dfrdg2  29445  brbigcup  29753  dfbigcup2  29754  fobigcup  29755  brapply  29793  dfrdg4  29805  ordtoplem  30105  onsucsuccmpi  30113  limsucncmpi  30115  ordcmp  30117  heicant  30254  ovoliunnfl  30261  voliunnfl  30263  volsupnfl  30264  mbfresfi  30266  isfne  30362  fneval  30375  fnemeet1  30389  fnemeet2  30390  fnejoin1  30391  fnejoin2  30392  tailfval  30395  cover2  30409  cover2g  30410  istotbnd3  30472  sstotbnd  30476  heiborlem1  30512  heiborlem6  30517  heiborlem8  30519  isnacs3  30847  nacsfix  30849  stoweidlem35  32020  stoweidlem39  32024  stoweidlem50  32035  stoweidlem57  32042  csbfv12gALTVD  33842  pwelg  37905