Theorem unieq 4094

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 2913	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2552	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 4088	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 4088	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1369   {cab 2424   E.wrex 2711   U.cuni 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-uni 4087

This theorem is referenced by:  unieqi  4095  unieqd  4096  uniintsn  4160  iununi  4250  treq  4386  limeq  4726  unizlim  4830  elvvuni  4894  unielrel  5357  unixp0  5366  unixpid  5367  opabiotafun  5747  uniex  6371  uniexg  6372  onsucuni2  6440  onuninsuci  6446  orduninsuc  6449  undefval  6787  en1b  7369  nnunifi  7555  fissuni  7608  infeq5i  7834  infeq5  7835  trcl  7940  rankuni  8062  rankxplim3  8080  iunfictbso  8276  cflim2  8424  cfss  8426  cfslb  8427  fin2i  8456  fin1a2lem10  8570  fin1a2lem11  8571  fin1a2lem12  8572  itunisuc  8580  ituniiun  8583  hsmex  8593  dominf  8606  zornn0g  8666  dominfac  8729  wununi  8865  wunex2  8897  wuncval2  8906  incexclem  13291  mrcfval  14538  mrisval  14560  acsdrsel  15329  isacs4lem  15330  isacs5lem  15331  acsdrscl  15332  isps  15364  isdir  15394  sylow2a  16109  uniopn  18490  eltopspOLD  18503  istpsOLD  18505  istopon  18510  eltg3  18547  tgdom  18563  indistopon  18585  cldval  18607  ntrfval  18608  clsfval  18609  mretopd  18676  neifval  18683  lpfval  18722  isperf  18735  tgrest  18743  ist0  18904  ist1  18905  ishaus  18906  iscnrm  18907  iscmp  18971  cmpcov  18972  cmpcovf  18974  cncmp  18975  fincmp  18976  cmpsublem  18982  cmpsub  18983  tgcmp  18984  cmpcld  18985  uncmp  18986  hauscmplem  18989  cmpfi  18991  bwthOLD  18994  iscon  18997  is1stc  19025  2ndc1stc  19035  2ndcsep  19043  kgenval  19088  1stckgenlem  19106  txcmplem1  19194  txcmplem2  19195  kqval  19279  flffval  19542  fclsval  19561  fcfval  19586  alexsublem  19596  alexsubb  19598  alexsubALTlem2  19600  alexsubALTlem3  19601  alexsubALTlem4  19602  alexsubALT  19603  ptcmplem2  19605  ptcmplem3  19606  ptcmplem5  19608  cnextval  19613  iscfilu  19843  icccmplem1  20379  icccmplem2  20380  bndth  20510  lebnumlem3  20515  om1val  20582  pi1val  20589  ovolicc2  20985  isplig  23632  hsupval  24705  sigaclcu  26529  prsiga  26543  sigaclci  26544  unelsiga  26546  sigagenval  26552  measvun  26592  ismbfm  26636  isanmbfm  26640  dya2iocuni  26667  oms0  26679  kur14  27073  ispcon  27081  cvmscbv  27116  cvmsi  27123  cvmsval  27124  relexp0  27300  relexpsucr  27301  dfrdg2  27578  brbigcup  27898  dfbigcup2  27899  fobigcup  27900  brapply  27938  dfrdg4  27950  ordtoplem  28251  onsucsuccmpi  28259  limsucncmpi  28261  ordcmp  28263  heicant  28397  ovoliunnfl  28404  voliunnfl  28406  volsupnfl  28407  mbfresfi  28409  isfne  28511  isref  28522  fneval  28530  isptfin  28538  islocfin  28539  comppfsc  28550  fnemeet1  28558  fnemeet2  28559  fnejoin1  28560  fnejoin2  28561  tailfval  28564  cover2  28578  cover2g  28579  istotbnd3  28641  sstotbnd  28645  heiborlem1  28681  heiborlem6  28686  heiborlem8  28688  isnacs3  29017  nacsfix  29019  stoweidlem35  29801  stoweidlem39  29805  stoweidlem50  29816  stoweidlem57  29823  csbfv12gALTVD  31564