Theorem unieq 4246

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 3052	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2596	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4240	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4240	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2526	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1374   {cab 2445   E.wrex 2808   U.cuni 4238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-uni 4239

This theorem is referenced by:  unieqi  4247  unieqd  4248  uniintsn  4312  iununi  4403  treq  4539  limeq  4883  unizlim  4987  elvvuni  5052  unielrel  5523  unixp0  5532  unixpid  5533  opabiotafun  5919  uniex  6571  uniexg  6572  onsucuni2  6640  onuninsuci  6646  orduninsuc  6649  undefval  6995  en1b  7573  nnunifi  7760  fissuni  7814  infeq5i  8042  infeq5  8043  trcl  8148  rankuni  8270  rankxplim3  8288  iunfictbso  8484  cflim2  8632  cfss  8634  cfslb  8635  fin2i  8664  fin1a2lem10  8778  fin1a2lem11  8779  fin1a2lem12  8780  itunisuc  8788  ituniiun  8791  hsmex  8801  dominf  8814  zornn0g  8874  dominfac  8937  wununi  9073  wunex2  9105  wuncval2  9114  incexclem  13600  mrcfval  14852  mrisval  14874  acsdrsel  15643  isacs4lem  15644  isacs5lem  15645  acsdrscl  15646  isps  15678  isdir  15708  sylow2a  16428  uniopn  19166  eltopspOLD  19179  istpsOLD  19181  istopon  19186  eltg3  19223  tgdom  19239  indistopon  19261  cldval  19283  ntrfval  19284  clsfval  19285  mretopd  19352  neifval  19359  lpfval  19398  isperf  19411  tgrest  19419  ist0  19580  ist1  19581  ishaus  19582  iscnrm  19583  iscmp  19647  cmpcov  19648  cmpcovf  19650  cncmp  19651  fincmp  19652  cmpsublem  19658  cmpsub  19659  tgcmp  19660  cmpcld  19661  uncmp  19662  hauscmplem  19665  cmpfi  19667  bwthOLD  19670  iscon  19673  is1stc  19701  2ndc1stc  19711  2ndcsep  19719  kgenval  19764  1stckgenlem  19782  txcmplem1  19870  txcmplem2  19871  kqval  19955  flffval  20218  fclsval  20237  fcfval  20262  alexsublem  20272  alexsubb  20274  alexsubALTlem2  20276  alexsubALTlem3  20277  alexsubALTlem4  20278  alexsubALT  20279  ptcmplem2  20281  ptcmplem3  20282  ptcmplem5  20284  cnextval  20289  iscfilu  20519  icccmplem1  21055  icccmplem2  21056  bndth  21186  lebnumlem3  21191  om1val  21258  pi1val  21265  ovolicc2  21661  isplig  24705  hsupval  25778  sigaclcu  27607  prsiga  27621  sigaclci  27622  unelsiga  27624  sigagenval  27630  measvun  27670  ismbfm  27713  isanmbfm  27717  dya2iocuni  27744  oms0  27756  kur14  28150  ispcon  28158  cvmscbv  28193  cvmsi  28200  cvmsval  28201  relexp0  28377  relexpsucr  28378  dfrdg2  28655  brbigcup  28975  dfbigcup2  28976  fobigcup  28977  brapply  29015  dfrdg4  29027  ordtoplem  29327  onsucsuccmpi  29335  limsucncmpi  29337  ordcmp  29339  heicant  29477  ovoliunnfl  29484  voliunnfl  29486  volsupnfl  29487  mbfresfi  29489  isfne  29591  isref  29602  fneval  29610  isptfin  29618  islocfin  29619  comppfsc  29630  fnemeet1  29638  fnemeet2  29639  fnejoin1  29640  fnejoin2  29641  tailfval  29644  cover2  29658  cover2g  29659  istotbnd3  29721  sstotbnd  29725  heiborlem1  29761  heiborlem6  29766  heiborlem8  29768  isnacs3  30097  nacsfix  30099  stoweidlem35  31154  stoweidlem39  31158  stoweidlem50  31169  stoweidlem57  31176  csbfv12gALTVD  32654