Theorem unieq 4087

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 2908	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2547	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4081	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4081	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2490	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1362   {cab 2419   E.wrex 2706   U.cuni 4079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-uni 4080

This theorem is referenced by:  unieqi  4088  unieqd  4089  uniintsn  4153  iununi  4243  treq  4379  limeq  4718  unizlim  4822  elvvuni  4886  unielrel  5350  unixp0  5359  unixpid  5360  opabiotafun  5740  uniex  6365  uniexg  6366  onsucuni2  6434  onuninsuci  6440  orduninsuc  6443  undefval  6781  en1b  7365  nnunifi  7551  fissuni  7604  infeq5i  7830  infeq5  7831  trcl  7936  rankuni  8058  rankxplim3  8076  iunfictbso  8272  cflim2  8420  cfss  8422  cfslb  8423  fin2i  8452  fin1a2lem10  8566  fin1a2lem11  8567  fin1a2lem12  8568  itunisuc  8576  ituniiun  8579  hsmex  8589  dominf  8602  zornn0g  8662  dominfac  8725  wununi  8861  wunex2  8893  wuncval2  8902  incexclem  13282  mrcfval  14529  mrisval  14551  acsdrsel  15320  isacs4lem  15321  isacs5lem  15322  acsdrscl  15323  isps  15355  isdir  15385  sylow2a  16098  uniopn  18352  eltopspOLD  18365  istpsOLD  18367  istopon  18372  eltg3  18409  tgdom  18425  indistopon  18447  cldval  18469  ntrfval  18470  clsfval  18471  mretopd  18538  neifval  18545  lpfval  18584  isperf  18597  tgrest  18605  ist0  18766  ist1  18767  ishaus  18768  iscnrm  18769  iscmp  18833  cmpcov  18834  cmpcovf  18836  cncmp  18837  fincmp  18838  cmpsublem  18844  cmpsub  18845  tgcmp  18846  cmpcld  18847  uncmp  18848  hauscmplem  18851  cmpfi  18853  bwthOLD  18856  iscon  18859  is1stc  18887  2ndc1stc  18897  2ndcsep  18905  kgenval  18950  1stckgenlem  18968  txcmplem1  19056  txcmplem2  19057  kqval  19141  flffval  19404  fclsval  19423  fcfval  19448  alexsublem  19458  alexsubb  19460  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  ptcmplem2  19467  ptcmplem3  19468  ptcmplem5  19470  cnextval  19475  iscfilu  19705  icccmplem1  20241  icccmplem2  20242  bndth  20372  lebnumlem3  20377  om1val  20444  pi1val  20451  ovolicc2  20847  isplig  23487  hsupval  24560  sigaclcu  26414  prsiga  26428  sigaclci  26429  unelsiga  26431  sigagenval  26437  measvun  26477  ismbfm  26521  isanmbfm  26525  dya2iocuni  26552  kur14  26952  ispcon  26960  cvmscbv  26995  cvmsi  27002  cvmsval  27003  relexp0  27178  relexpsucr  27179  dfrdg2  27456  brbigcup  27776  dfbigcup2  27777  fobigcup  27778  brapply  27816  dfrdg4  27828  ordtoplem  28129  onsucsuccmpi  28137  limsucncmpi  28139  ordcmp  28141  heicant  28270  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  mbfresfi  28282  isfne  28384  isref  28395  fneval  28403  isptfin  28411  islocfin  28412  comppfsc  28423  fnemeet1  28431  fnemeet2  28432  fnejoin1  28433  fnejoin2  28434  tailfval  28437  cover2  28451  cover2g  28452  istotbnd3  28514  sstotbnd  28518  heiborlem1  28554  heiborlem6  28559  heiborlem8  28561  isnacs3  28891  nacsfix  28893  stoweidlem35  29676  stoweidlem39  29680  stoweidlem50  29691  stoweidlem57  29698  csbfv12gALTVD  31337