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 3971	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4882	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3972	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4882	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3930	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∪ cuni 4872

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873

This theorem is used by:  unieqi  4884  unieqd  4885  uniintsn  4950  iununi  5064  treq  5225  eqsnuniex  5330  elvvuni  5736  unielrel  6300  unixp0  6310  unixpid  6311  limeq  6400  unizlim  6513  iotauni2  6536  opabiotafun  6996  uniexg  7789  onsucuni2  7879  onuninsuci  7885  orduninsuc  7888  undefval  8332  en1b  9090  fissorduni  9320  nnunifi  9321  fissuni  9384  infeq5i  9674  infeq5  9675  rnttrcl  9760  ttrclselem2  9764  trcl  9766  rankuni  9916  rankxplim3  9935  iunfictbso  10232  cflim2  10380  cfss  10382  cfslb  10383  fin2i  10412  fin1a2lem10  10526  fin1a2lem11  10527  fin1a2lem12  10528  itunisuc  10536  ituniiun  10539  hsmex  10549  dominf  10562  zornn0g  10622  dominfac  10697  wununi  10830  wunex2  10862  wuncval2  10871  incexclem  16049  mrcfval  17832  mrisval  17854  acsdrsel  18767  isacs4lem  18768  isacs5lem  18769  acsdrscl  18770  isps  18792  isdir  18822  sylow2a  19884  uniopn  23270  istopon  23285  eltg3  23335  tgdom  23351  indistopon  23374  cldval  23396  ntrfval  23397  clsfval  23398  mretopd  23465  neifval  23472  lpfval  23511  isperf  23524  tgrest  23532  ist0  23693  ist1  23694  ishaus  23695  iscnrm  23696  iscmp  23761  cmpcov  23762  cmpcovf  23764  cncmp  23765  fincmp  23766  cmpsublem  23772  cmpsub  23773  tgcmp  23774  cmpcld  23775  uncmp  23776  hauscmplem  23779  cmpfi  23781  isconn  23786  is1stc  23814  2ndc1stc  23824  2ndcsep  23833  isref  23883  isptfin  23890  islocfin  23891  comppfsc  23906  kgenval  23909  1stckgenlem  23927  txcmplem1  24015  txcmplem2  24016  kqval  24100  flffval  24363  fclsval  24382  fcfval  24407  alexsublem  24418  alexsubb  24420  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  alexsubALT  24425  ptcmplem2  24427  ptcmplem3  24428  ptcmplem5  24430  cnextval  24435  iscfilu  24661  icccmplem1  25197  icccmplem2  25198  bndth  25334  lebnumlem3  25339  om1val  25406  pi1val  25413  ovolicc2  25898  isplig  31135  hsupval  31993  acunirnmpt  33351  iscref  34587  crefi  34590  cmpcref  34593  pcmplfin  34603  sigaclcu  34860  prsiga  34874  sigaclci  34875  unelsiga  34877  sigagenval  34884  unelldsys  34902  sigapildsys  34906  ldgenpisyslem1  34907  rossros  34924  measvun  34953  ismbfm  34995  dya2iocuni  35026  oms0  35040  omssubadd  35043  carsgsigalem  35058  fiunelcarsg  35059  carsgclctunlem1  35060  carsgclctunlem2  35062  carsgclctunlem3  35063  carsgclctun  35064  pmeasmono  35067  pmeasadd  35068  fineqvnttrclselem2  35931  wevgblacfn  36080  kur14  36189  ispconn  36196  cvmscbv  36231  cvmsi  36238  cvmsval  36239  nnuni  36707  dfrdg2  36772  brbigcup  36875  dfbigcup2  36876  fobigcup  36877  brapply  36915  dfrdg4  36930  isfne  37342  fneval  37355  fnemeet1  37369  fnemeet2  37370  fnejoin1  37371  fnejoin2  37372  tailfval  37375  ordtoplem  37438  onsucsuccmpi  37446  limsucncmpi  37448  ordcmp  37450  ttctr  37496  ttcmin  37499  dfttc2g  37509  bj-ismoore  38296  dissneqlem  38531  finxpreclem3  38584  pibp19  38605  pibp21  38606  pibt2  38608  heicant  38841  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  mbfresfi  38852  cover2  38917  cover2g  38918  istotbnd3  38971  sstotbnd  38975  heiborlem1  39011  heiborlem6  39016  heiborlem8  39018  dmqseqim  39939  isnacs3  43987  nacsfix  43989  onsupnmax  44491  onov0suclim  44537  pwelg  44822  mnuprdlem1  45517  mnuprdlem2  45518  mnuunid  45522  mnurndlem1  45526  ismnushort  45546  csbfv12gALTVD  46141  stoweidlem35  47318  stoweidlem39  47322  stoweidlem50  47333  stoweidlem57  47340  issal  47597  salunicl  47599  saluncl  47600  prsal  47601  salgenval  47604  intsaluni  47612  salgenn0  47614  salgencl  47615  sssalgen  47618  salgenss  47619  salgenuni  47620  issalgend  47621  dfsalgen2  47624  issalnnd  47628  meadjuni  47740  ismeannd  47750  omeunile  47788  caragenunicl  47807  isomennd  47814  issmflem  48010  termco  50947  onsetreclem1  51204