Theorem unieq 3984

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 2865	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2518	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 3977	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 3977	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2461	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1649   {cab 2390   E.wrex 2667   U.cuni 3975

This theorem is referenced by:  unieqi  3985  unieqd  3986  uniintsn  4047  iununi  4135  treq  4268  limeq  4553  unizlim  4657  uniex  4664  uniexg  4665  onsucuni2  4773  onuninsuci  4779  orduninsuc  4782  elvvuni  4897  unielrel  5353  unixp0  5362  unixpid  5363  opabiotafun  6495  undefval  6505  en1b  7134  nnunifi  7317  fissuni  7369  infeq5i  7547  infeq5  7548  trcl  7620  rankuni  7745  rankxplim3  7761  iunfictbso  7951  cflim2  8099  cfss  8101  cfslb  8102  fin2i  8131  fin1a2lem10  8245  fin1a2lem11  8246  fin1a2lem12  8247  itunisuc  8255  ituniiun  8258  hsmex  8268  dominf  8281  zornn0g  8341  dominfac  8404  wununi  8537  wunex2  8569  wuncval2  8578  incexclem  12571  mrcfval  13788  mrisval  13810  acsdrsel  14548  isacs4lem  14549  isacs5lem  14550  acsdrscl  14551  isps  14589  spwval2  14611  isdir  14632  sylow2a  15208  uniopn  16925  eltopspOLD  16938  istpsOLD  16940  istopon  16945  eltg3  16982  tgdom  16998  indistopon  17020  cldval  17042  ntrfval  17043  clsfval  17044  mretopd  17111  neifval  17118  lpfval  17157  isperf  17169  tgrest  17177  ist0  17338  ist1  17339  ishaus  17340  iscnrm  17341  iscmp  17405  cmpcov  17406  cmpcovf  17408  cncmp  17409  fincmp  17410  cmpsublem  17416  cmpsub  17417  tgcmp  17418  cmpcld  17419  uncmp  17420  hauscmplem  17423  cmpfi  17425  iscon  17429  is1stc  17457  2ndc1stc  17467  2ndcsep  17475  kgenval  17520  1stckgenlem  17538  txcmplem1  17626  txcmplem2  17627  kqval  17711  flffval  17974  fclsval  17993  fcfval  18018  alexsublem  18028  alexsubb  18030  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  ptcmplem5  18040  cnextval  18045  iscfilu  18271  icccmplem1  18806  icccmplem2  18807  bndth  18936  lebnumlem3  18941  om1val  19008  pi1val  19015  ovolicc2  19371  isplig  21718  hsupval  22789  sigaclcu  24453  prsiga  24467  sigaclci  24468  unelsiga  24470  sigagenval  24476  measvun  24516  ismbfm  24555  isanmbfm  24559  dya2iocuni  24586  kur14  24855  ispcon  24863  cvmscbv  24898  cvmsi  24905  cvmsval  24906  relexp0  25082  relexpsucr  25083  dfrdg2  25366  brbigcup  25652  dfbigcup2  25653  fobigcup  25654  brapply  25691  dfrdg4  25703  ordtoplem  26089  onsucsuccmpi  26097  limsucncmpi  26099  ordcmp  26101  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  isfne  26238  isref  26249  fneval  26257  isptfin  26265  islocfin  26266  comppfsc  26277  fnemeet1  26285  fnemeet2  26286  fnejoin1  26287  fnejoin2  26288  tailfval  26291  cover2  26305  cover2g  26306  istotbnd3  26370  sstotbnd  26374  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  isnacs3  26654  nacsfix  26656  stoweidlem35  27651  stoweidlem39  27655  stoweidlem50  27666  stoweidlem57  27673  csbfv12gALTVD  28720

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-uni 3976