Theorem unieq 4238

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 3039	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2577	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4232	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4232	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2507	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1381   {cab 2426   E.wrex 2792   U.cuni 4230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-uni 4231

This theorem is referenced by:  unieqi  4239  unieqd  4240  uniintsn  4305  iununi  4396  treq  4532  limeq  4876  unizlim  4980  elvvuni  5046  unielrel  5518  unixp0  5527  unixpid  5528  opabiotafun  5915  uniex  6577  uniexg  6578  onsucuni2  6650  onuninsuci  6656  orduninsuc  6659  undefval  7003  en1b  7581  nnunifi  7769  fissuni  7823  infeq5i  8051  infeq5  8052  trcl  8157  rankuni  8279  rankxplim3  8297  iunfictbso  8493  cflim2  8641  cfss  8643  cfslb  8644  fin2i  8673  fin1a2lem10  8787  fin1a2lem11  8788  fin1a2lem12  8789  itunisuc  8797  ituniiun  8800  hsmex  8810  dominf  8823  zornn0g  8883  dominfac  8946  wununi  9082  wunex2  9114  wuncval2  9123  incexclem  13622  mrcfval  14877  mrisval  14899  acsdrsel  15666  isacs4lem  15667  isacs5lem  15668  acsdrscl  15669  isps  15701  isdir  15731  sylow2a  16508  uniopn  19273  eltopspOLD  19286  istpsOLD  19288  istopon  19293  eltg3  19330  tgdom  19346  indistopon  19368  cldval  19390  ntrfval  19391  clsfval  19392  mretopd  19459  neifval  19466  lpfval  19505  isperf  19518  tgrest  19526  ist0  19687  ist1  19688  ishaus  19689  iscnrm  19690  iscmp  19754  cmpcov  19755  cmpcovf  19757  cncmp  19758  fincmp  19759  cmpsublem  19765  cmpsub  19766  tgcmp  19767  cmpcld  19768  uncmp  19769  hauscmplem  19772  cmpfi  19774  bwthOLD  19777  iscon  19780  is1stc  19808  2ndc1stc  19818  2ndcsep  19826  isref  19876  isptfin  19883  islocfin  19884  comppfsc  19899  kgenval  19902  1stckgenlem  19920  txcmplem1  20008  txcmplem2  20009  kqval  20093  flffval  20356  fclsval  20375  fcfval  20400  alexsublem  20410  alexsubb  20412  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  alexsubALT  20417  ptcmplem2  20419  ptcmplem3  20420  ptcmplem5  20422  cnextval  20427  iscfilu  20657  icccmplem1  21193  icccmplem2  21194  bndth  21324  lebnumlem3  21329  om1val  21396  pi1val  21403  ovolicc2  21799  isplig  25044  hsupval  26117  iscref  27713  crefi  27716  cmpcref  27719  pcmplfin  27729  sigaclcu  27983  prsiga  27997  sigaclci  27998  unelsiga  28000  sigagenval  28006  measvun  28046  ismbfm  28089  isanmbfm  28093  dya2iocuni  28120  oms0  28132  kur14  28526  ispcon  28534  cvmscbv  28569  cvmsi  28576  cvmsval  28577  relexp0  28918  relexpsucr  28919  dfrdg2  29196  brbigcup  29516  dfbigcup2  29517  fobigcup  29518  brapply  29556  dfrdg4  29568  ordtoplem  29868  onsucsuccmpi  29876  limsucncmpi  29878  ordcmp  29880  heicant  30017  ovoliunnfl  30024  voliunnfl  30026  volsupnfl  30027  mbfresfi  30029  isfne  30125  fneval  30138  fnemeet1  30152  fnemeet2  30153  fnejoin1  30154  fnejoin2  30155  tailfval  30158  cover2  30172  cover2g  30173  istotbnd3  30235  sstotbnd  30239  heiborlem1  30275  heiborlem6  30280  heiborlem8  30282  isnacs3  30610  nacsfix  30612  stoweidlem35  31702  stoweidlem39  31706  stoweidlem50  31717  stoweidlem57  31724  csbfv12gALTVD  33407  pwelg  37410