Theorem unieq 4206

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 2988	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2569	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4200	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4200	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2510	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1444   {cab 2437   E.wrex 2738   U.cuni 4198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-uni 4199

This theorem is referenced by:  unieqi  4207  unieqd  4208  uniintsn  4272  iununi  4366  treq  4503  elvvuni  4895  unielrel  5360  unixp0  5370  unixpid  5371  limeq  5435  unizlim  5539  opabiotafun  5926  uniex  6587  uniexg  6588  onsucuni2  6661  onuninsuci  6667  orduninsuc  6670  undefval  7023  en1b  7637  nnunifi  7822  fissuni  7879  infeq5i  8141  infeq5  8142  trcl  8212  rankuni  8334  rankxplim3  8352  iunfictbso  8545  cflim2  8693  cfss  8695  cfslb  8696  fin2i  8725  fin1a2lem10  8839  fin1a2lem11  8840  fin1a2lem12  8841  itunisuc  8849  ituniiun  8852  hsmex  8862  dominf  8875  zornn0g  8935  dominfac  8998  wununi  9131  wunex2  9163  wuncval2  9172  incexclem  13894  mrcfval  15514  mrisval  15536  acsdrsel  16413  isacs4lem  16414  isacs5lem  16415  acsdrscl  16416  isps  16448  isdir  16478  sylow2a  17271  uniopn  19927  istopon  19940  eltg3  19977  tgdom  19994  indistopon  20016  cldval  20038  ntrfval  20039  clsfval  20040  mretopd  20108  neifval  20115  lpfval  20154  isperf  20167  tgrest  20175  ist0  20336  ist1  20337  ishaus  20338  iscnrm  20339  iscmp  20403  cmpcov  20404  cmpcovf  20406  cncmp  20407  fincmp  20408  cmpsublem  20414  cmpsub  20415  tgcmp  20416  cmpcld  20417  uncmp  20418  hauscmplem  20421  cmpfi  20423  iscon  20428  is1stc  20456  2ndc1stc  20466  2ndcsep  20474  isref  20524  isptfin  20531  islocfin  20532  comppfsc  20547  kgenval  20550  1stckgenlem  20568  txcmplem1  20656  txcmplem2  20657  kqval  20741  flffval  21004  fclsval  21023  fcfval  21048  alexsublem  21059  alexsubb  21061  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  alexsubALT  21066  ptcmplem2  21068  ptcmplem3  21069  ptcmplem5  21071  cnextval  21076  iscfilu  21303  icccmplem1  21840  icccmplem2  21841  bndth  21986  lebnumlem3  21991  lebnumlem3OLD  21994  om1val  22061  pi1val  22068  ovolicc2  22476  isplig  25909  hsupval  26987  acunirnmpt  28261  iscref  28671  crefi  28674  cmpcref  28677  pcmplfin  28687  sigaclcu  28939  prsiga  28953  sigaclci  28954  unelsiga  28956  sigagenval  28962  unelldsys  28980  sigapildsys  28984  ldgenpisyslem1  28985  rossros  29002  measvun  29031  ismbfm  29074  isanmbfm  29078  dya2iocuni  29105  oms0  29125  omssubadd  29128  oms0OLD  29129  omssubaddOLD  29132  carsgsigalem  29147  fiunelcarsg  29148  carsgclctunlem1  29149  carsgclctunlem2  29151  carsgclctunlem3  29152  carsgclctun  29153  pmeasmono  29157  pmeasadd  29158  kur14  29939  ispcon  29946  cvmscbv  29981  cvmsi  29988  cvmsval  29989  dfrdg2  30442  brbigcup  30665  dfbigcup2  30666  fobigcup  30667  brapply  30705  dfrdg4  30718  isfne  30995  fneval  31008  fnemeet1  31022  fnemeet2  31023  fnejoin1  31024  fnejoin2  31025  tailfval  31028  ordtoplem  31095  onsucsuccmpi  31103  limsucncmpi  31105  ordcmp  31107  dissneqlem  31742  finxpreclem3  31785  heicant  31975  ovoliunnfl  31982  voliunnfl  31984  volsupnfl  31985  mbfresfi  31987  cover2  32040  cover2g  32041  istotbnd3  32103  sstotbnd  32107  heiborlem1  32143  heiborlem6  32148  heiborlem8  32150  isnacs3  35552  nacsfix  35554  pwelg  36164  csbfv12gALTVD  37296  stoweidlem35  37896  stoweidlem39  37900  stoweidlem50  37911  stoweidlem57  37918  issal  38175  salunicl  38177  saluncl  38178  prsal  38179  salgenval  38182  intsaluni  38188  salgenn0  38190  salgencl  38191  sssalgen  38194  salgenss  38195  salgenuni  38196  issalgend  38197  dfsalgen2  38200  meadjuni  38295  ismeannd  38305  omeunile  38326  caragenunicl  38345  isomennd  38352