Theorem unieq 4197

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 3014	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2587	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4191	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4191	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2517	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1370   {cab 2436   E.wrex 2796   U.cuni 4189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-uni 4190

This theorem is referenced by:  unieqi  4198  unieqd  4199  uniintsn  4263  iununi  4353  treq  4489  limeq  4829  unizlim  4933  elvvuni  4997  unielrel  5460  unixp0  5469  unixpid  5470  opabiotafun  5851  uniex  6476  uniexg  6477  onsucuni2  6545  onuninsuci  6551  orduninsuc  6554  undefval  6895  en1b  7477  nnunifi  7664  fissuni  7717  infeq5i  7943  infeq5  7944  trcl  8049  rankuni  8171  rankxplim3  8189  iunfictbso  8385  cflim2  8533  cfss  8535  cfslb  8536  fin2i  8565  fin1a2lem10  8679  fin1a2lem11  8680  fin1a2lem12  8681  itunisuc  8689  ituniiun  8692  hsmex  8702  dominf  8715  zornn0g  8775  dominfac  8838  wununi  8974  wunex2  9006  wuncval2  9015  incexclem  13401  mrcfval  14648  mrisval  14670  acsdrsel  15439  isacs4lem  15440  isacs5lem  15441  acsdrscl  15442  isps  15474  isdir  15504  sylow2a  16222  uniopn  18626  eltopspOLD  18639  istpsOLD  18641  istopon  18646  eltg3  18683  tgdom  18699  indistopon  18721  cldval  18743  ntrfval  18744  clsfval  18745  mretopd  18812  neifval  18819  lpfval  18858  isperf  18871  tgrest  18879  ist0  19040  ist1  19041  ishaus  19042  iscnrm  19043  iscmp  19107  cmpcov  19108  cmpcovf  19110  cncmp  19111  fincmp  19112  cmpsublem  19118  cmpsub  19119  tgcmp  19120  cmpcld  19121  uncmp  19122  hauscmplem  19125  cmpfi  19127  bwthOLD  19130  iscon  19133  is1stc  19161  2ndc1stc  19171  2ndcsep  19179  kgenval  19224  1stckgenlem  19242  txcmplem1  19330  txcmplem2  19331  kqval  19415  flffval  19678  fclsval  19697  fcfval  19722  alexsublem  19732  alexsubb  19734  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALTlem4  19738  alexsubALT  19739  ptcmplem2  19741  ptcmplem3  19742  ptcmplem5  19744  cnextval  19749  iscfilu  19979  icccmplem1  20515  icccmplem2  20516  bndth  20646  lebnumlem3  20651  om1val  20718  pi1val  20725  ovolicc2  21121  isplig  23799  hsupval  24872  sigaclcu  26694  prsiga  26708  sigaclci  26709  unelsiga  26711  sigagenval  26717  measvun  26757  ismbfm  26801  isanmbfm  26805  dya2iocuni  26832  oms0  26844  kur14  27238  ispcon  27246  cvmscbv  27281  cvmsi  27288  cvmsval  27289  relexp0  27465  relexpsucr  27466  dfrdg2  27743  brbigcup  28063  dfbigcup2  28064  fobigcup  28065  brapply  28103  dfrdg4  28115  ordtoplem  28415  onsucsuccmpi  28423  limsucncmpi  28425  ordcmp  28427  heicant  28564  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  mbfresfi  28576  isfne  28678  isref  28689  fneval  28697  isptfin  28705  islocfin  28706  comppfsc  28717  fnemeet1  28725  fnemeet2  28726  fnejoin1  28727  fnejoin2  28728  tailfval  28731  cover2  28745  cover2g  28746  istotbnd3  28808  sstotbnd  28812  heiborlem1  28848  heiborlem6  28853  heiborlem8  28855  isnacs3  29184  nacsfix  29186  stoweidlem35  29968  stoweidlem39  29972  stoweidlem50  29983  stoweidlem57  29990  csbfv12gALTVD  31935