Theorem unieq 4883

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.) (Proof shortened by BJ, 13-Apr-2024.)

Assertion

Ref	Expression
unieq	⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieq

Step	Hyp	Ref	Expression
1		eqimss 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4882	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4882	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3954	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1570  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873

This theorem is referenced by:  unieqi  4884  unieqd  4885  uniintsn  4950  iununi  5065  treq  5225  eqsnuniex  5332  elvvuni  5738  unielrel  6275  unixp0  6284  unixpid  6285  limeq  6372  unizlim  6485  iotauni2  6508  opabiotafun  6961  uniexg  7738  onsucuni2  7826  onuninsuci  7832  orduninsuc  7835  undefval  8269  en1b  9018  nnunifi  9247  fissuni  9310  infeq5i  9601  infeq5  9602  rnttrcl  9687  ttrclselem2  9691  trcl  9693  rankuni  9831  rankxplim3  9849  iunfictbso  10094  cflim2  10242  cfss  10244  cfslb  10245  fin2i  10274  fin1a2lem10  10388  fin1a2lem11  10389  fin1a2lem12  10390  itunisuc  10398  ituniiun  10401  hsmex  10411  dominf  10424  zornn0g  10484  dominfac  10553  wununi  10686  wunex2  10718  wuncval2  10727  incexclem  15886  mrcfval  17659  mrisval  17681  acsdrsel  18594  isacs4lem  18595  isacs5lem  18596  acsdrscl  18597  isps  18619  isdir  18649  sylow2a  19684  uniopn  23054  istopon  23069  eltg3  23119  tgdom  23135  indistopon  23158  cldval  23180  ntrfval  23181  clsfval  23182  mretopd  23249  neifval  23256  lpfval  23295  isperf  23308  tgrest  23316  ist0  23477  ist1  23478  ishaus  23479  iscnrm  23480  iscmp  23545  cmpcov  23546  cmpcovf  23548  cncmp  23549  fincmp  23550  cmpsublem  23556  cmpsub  23557  tgcmp  23558  cmpcld  23559  uncmp  23560  hauscmplem  23563  cmpfi  23565  isconn  23570  is1stc  23598  2ndc1stc  23608  2ndcsep  23616  isref  23666  isptfin  23673  islocfin  23674  comppfsc  23689  kgenval  23692  1stckgenlem  23710  txcmplem1  23798  txcmplem2  23799  kqval  23883  flffval  24146  fclsval  24165  fcfval  24190  alexsublem  24201  alexsubb  24203  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  alexsubALT  24208  ptcmplem2  24210  ptcmplem3  24211  ptcmplem5  24213  cnextval  24218  iscfilu  24444  icccmplem1  24980  icccmplem2  24981  bndth  25117  lebnumlem3  25122  om1val  25189  pi1val  25196  ovolicc2  25681  isplig  30828  hsupval  31686  acunirnmpt  33004  iscref  34234  crefi  34237  cmpcref  34240  pcmplfin  34250  sigaclcu  34507  prsiga  34521  sigaclci  34522  unelsiga  34524  sigagenval  34530  unelldsys  34548  sigapildsys  34552  ldgenpisyslem1  34553  rossros  34570  measvun  34599  ismbfm  34641  dya2iocuni  34673  oms0  34687  omssubadd  34690  carsgsigalem  34705  fiunelcarsg  34706  carsgclctunlem1  34707  carsgclctunlem2  34709  carsgclctunlem3  34710  carsgclctun  34711  pmeasmono  34714  pmeasadd  34715  fissorduni  35480  fineqvnttrclselem2  35535  wevgblacfn  35595  kur14  35708  ispconn  35715  cvmscbv  35750  cvmsi  35757  cvmsval  35758  nnuni  36219  dfrdg2  36285  brbigcup  36388  dfbigcup2  36389  fobigcup  36390  brapply  36428  dfrdg4  36443  isfne  36870  fneval  36883  fnemeet1  36897  fnemeet2  36898  fnejoin1  36899  fnejoin2  36900  tailfval  36903  ordtoplem  36966  onsucsuccmpi  36974  limsucncmpi  36976  ordcmp  36978  ttctr  37024  ttcmin  37027  dfttc2g  37037  bj-ismoore  37767  dissneqlem  38006  finxpreclem3  38059  pibp19  38080  pibp21  38081  pibt2  38083  heicant  38326  ovoliunnfl  38333  voliunnfl  38335  volsupnfl  38336  mbfresfi  38337  cover2  38386  cover2g  38387  istotbnd3  38442  sstotbnd  38446  heiborlem1  38482  heiborlem6  38487  heiborlem8  38489  dmqseqim  39410  isnacs3  43461  nacsfix  43463  onsupnmax  43975  onov0suclim  44021  pwelg  44306  mnuprdlem1  45002  mnuprdlem2  45003  mnuunid  45007  mnurndlem1  45011  ismnushort  45031  csbfv12gALTVD  45627  stoweidlem35  46769  stoweidlem39  46773  stoweidlem50  46784  stoweidlem57  46791  issal  47048  salunicl  47050  saluncl  47051  prsal  47052  salgenval  47055  intsaluni  47063  salgenn0  47065  salgencl  47066  sssalgen  47069  salgenss  47070  salgenuni  47071  issalgend  47072  dfsalgen2  47075  issalnnd  47079  meadjuni  47191  ismeannd  47201  omeunile  47239  caragenunicl  47258  isomennd  47265  issmflem  47461  termco  50279  onsetreclem1  50503