Theorem unieq 4874

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 3992	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4873	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3993	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4873	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3951	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1541  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864

This theorem is referenced by:  unieqi  4875  unieqd  4876  uniintsn  4940  iununi  5054  treq  5212  eqsnuniex  5306  elvvuni  5701  unielrel  6232  unixp0  6241  unixpid  6242  limeq  6329  unizlim  6441  iotauni2  6464  opabiotafun  6914  uniexg  7685  onsucuni2  7776  onuninsuci  7782  orduninsuc  7785  undefval  8218  en1b  8962  nnunifi  9191  fissuni  9257  infeq5i  9545  infeq5  9546  rnttrcl  9631  ttrclselem2  9635  trcl  9637  rankuni  9775  rankxplim3  9793  iunfictbso  10024  cflim2  10173  cfss  10175  cfslb  10176  fin2i  10205  fin1a2lem10  10319  fin1a2lem11  10320  fin1a2lem12  10321  itunisuc  10329  ituniiun  10332  hsmex  10342  dominf  10355  zornn0g  10415  dominfac  10484  wununi  10617  wunex2  10649  wuncval2  10658  incexclem  15759  mrcfval  17531  mrisval  17553  acsdrsel  18466  isacs4lem  18467  isacs5lem  18468  acsdrscl  18469  isps  18491  isdir  18521  sylow2a  19548  uniopn  22841  istopon  22856  eltg3  22906  tgdom  22922  indistopon  22945  cldval  22967  ntrfval  22968  clsfval  22969  mretopd  23036  neifval  23043  lpfval  23082  isperf  23095  tgrest  23103  ist0  23264  ist1  23265  ishaus  23266  iscnrm  23267  iscmp  23332  cmpcov  23333  cmpcovf  23335  cncmp  23336  fincmp  23337  cmpsublem  23343  cmpsub  23344  tgcmp  23345  cmpcld  23346  uncmp  23347  hauscmplem  23350  cmpfi  23352  isconn  23357  is1stc  23385  2ndc1stc  23395  2ndcsep  23403  isref  23453  isptfin  23460  islocfin  23461  comppfsc  23476  kgenval  23479  1stckgenlem  23497  txcmplem1  23585  txcmplem2  23586  kqval  23670  flffval  23933  fclsval  23952  fcfval  23977  alexsublem  23988  alexsubb  23990  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  ptcmplem2  23997  ptcmplem3  23998  ptcmplem5  24000  cnextval  24005  iscfilu  24231  icccmplem1  24767  icccmplem2  24768  bndth  24913  lebnumlem3  24918  om1val  24986  pi1val  24993  ovolicc2  25479  isplig  30551  hsupval  31409  acunirnmpt  32737  iscref  34001  crefi  34004  cmpcref  34007  pcmplfin  34017  sigaclcu  34274  prsiga  34288  sigaclci  34289  unelsiga  34291  sigagenval  34297  unelldsys  34315  sigapildsys  34319  ldgenpisyslem1  34320  rossros  34337  measvun  34366  ismbfm  34408  dya2iocuni  34440  oms0  34454  omssubadd  34457  carsgsigalem  34472  fiunelcarsg  34473  carsgclctunlem1  34474  carsgclctunlem2  34476  carsgclctunlem3  34477  carsgclctun  34478  pmeasmono  34481  pmeasadd  34482  fissorduni  35246  fineqvnttrclselem2  35278  wevgblacfn  35303  kur14  35410  ispconn  35417  cvmscbv  35452  cvmsi  35459  cvmsval  35460  nnuni  35921  dfrdg2  35987  brbigcup  36090  dfbigcup2  36091  fobigcup  36092  brapply  36130  dfrdg4  36145  isfne  36533  fneval  36546  fnemeet1  36560  fnemeet2  36561  fnejoin1  36562  fnejoin2  36563  tailfval  36566  ordtoplem  36629  onsucsuccmpi  36637  limsucncmpi  36639  ordcmp  36641  bj-ismoore  37310  dissneqlem  37545  finxpreclem3  37598  pibp19  37619  pibp21  37620  pibt2  37622  heicant  37856  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  mbfresfi  37867  cover2  37916  cover2g  37917  istotbnd3  37972  sstotbnd  37976  heiborlem1  38012  heiborlem6  38017  heiborlem8  38019  dmqseqim  38925  isnacs3  42962  nacsfix  42964  onsupnmax  43480  onov0suclim  43526  pwelg  43811  mnuprdlem1  44523  mnuprdlem2  44524  mnuunid  44528  mnurndlem1  44532  ismnushort  44552  csbfv12gALTVD  45149  stoweidlem35  46289  stoweidlem39  46293  stoweidlem50  46304  stoweidlem57  46311  issal  46568  salunicl  46570  saluncl  46571  prsal  46572  salgenval  46575  intsaluni  46583  salgenn0  46585  salgencl  46586  sssalgen  46589  salgenss  46590  salgenuni  46591  issalgend  46592  dfsalgen2  46595  issalnnd  46599  meadjuni  46711  ismeannd  46721  omeunile  46759  caragenunicl  46778  isomennd  46785  issmflem  46981  termco  49736  onsetreclem1  49960