Theorem unieq 4894

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 4017	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4893	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4018	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4893	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3976	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  unieqi  4895  unieqd  4896  uniintsn  4961  iununi  5075  treq  5237  eqsnuniex  5331  elvvuni  5731  unielrel  6263  unixp0  6272  unixpid  6273  limeq  6364  unizlim  6476  iotauni2  6499  opabiotafun  6958  uniexg  7732  onsucuni2  7826  onuninsuci  7833  orduninsuc  7836  undefval  8273  en1b  9037  nnunifi  9297  fissuni  9367  infeq5i  9648  infeq5  9649  rnttrcl  9734  ttrclselem2  9738  trcl  9740  rankuni  9875  rankxplim3  9893  iunfictbso  10126  cflim2  10275  cfss  10277  cfslb  10278  fin2i  10307  fin1a2lem10  10421  fin1a2lem11  10422  fin1a2lem12  10423  itunisuc  10431  ituniiun  10434  hsmex  10444  dominf  10457  zornn0g  10517  dominfac  10585  wununi  10718  wunex2  10750  wuncval2  10759  incexclem  15850  mrcfval  17618  mrisval  17640  acsdrsel  18551  isacs4lem  18552  isacs5lem  18553  acsdrscl  18554  isps  18576  isdir  18606  sylow2a  19598  uniopn  22833  istopon  22848  eltg3  22898  tgdom  22914  indistopon  22937  cldval  22959  ntrfval  22960  clsfval  22961  mretopd  23028  neifval  23035  lpfval  23074  isperf  23087  tgrest  23095  ist0  23256  ist1  23257  ishaus  23258  iscnrm  23259  iscmp  23324  cmpcov  23325  cmpcovf  23327  cncmp  23328  fincmp  23329  cmpsublem  23335  cmpsub  23336  tgcmp  23337  cmpcld  23338  uncmp  23339  hauscmplem  23342  cmpfi  23344  isconn  23349  is1stc  23377  2ndc1stc  23387  2ndcsep  23395  isref  23445  isptfin  23452  islocfin  23453  comppfsc  23468  kgenval  23471  1stckgenlem  23489  txcmplem1  23577  txcmplem2  23578  kqval  23662  flffval  23925  fclsval  23944  fcfval  23969  alexsublem  23980  alexsubb  23982  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  ptcmplem2  23989  ptcmplem3  23990  ptcmplem5  23992  cnextval  23997  iscfilu  24224  icccmplem1  24760  icccmplem2  24761  bndth  24906  lebnumlem3  24911  om1val  24979  pi1val  24986  ovolicc2  25473  isplig  30403  hsupval  31261  acunirnmpt  32583  iscref  33821  crefi  33824  cmpcref  33827  pcmplfin  33837  sigaclcu  34094  prsiga  34108  sigaclci  34109  unelsiga  34111  sigagenval  34117  unelldsys  34135  sigapildsys  34139  ldgenpisyslem1  34140  rossros  34157  measvun  34186  ismbfm  34228  dya2iocuni  34261  oms0  34275  omssubadd  34278  carsgsigalem  34293  fiunelcarsg  34294  carsgclctunlem1  34295  carsgclctunlem2  34297  carsgclctunlem3  34298  carsgclctun  34299  pmeasmono  34302  pmeasadd  34303  wevgblacfn  35077  kur14  35184  ispconn  35191  cvmscbv  35226  cvmsi  35233  cvmsval  35234  nnuni  35690  dfrdg2  35759  brbigcup  35862  dfbigcup2  35863  fobigcup  35864  brapply  35902  dfrdg4  35915  isfne  36303  fneval  36316  fnemeet1  36330  fnemeet2  36331  fnejoin1  36332  fnejoin2  36333  tailfval  36336  ordtoplem  36399  onsucsuccmpi  36407  limsucncmpi  36409  ordcmp  36411  bj-ismoore  37069  dissneqlem  37304  finxpreclem3  37357  pibp19  37378  pibp21  37379  pibt2  37381  heicant  37625  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  cover2  37685  cover2g  37686  istotbnd3  37741  sstotbnd  37745  heiborlem1  37781  heiborlem6  37786  heiborlem8  37788  dmqseqim  38620  isnacs3  42680  nacsfix  42682  onsupnmax  43199  onov0suclim  43245  pwelg  43531  mnuprdlem1  44244  mnuprdlem2  44245  mnuunid  44249  mnurndlem1  44253  ismnushort  44273  csbfv12gALTVD  44871  stoweidlem35  46012  stoweidlem39  46016  stoweidlem50  46027  stoweidlem57  46034  issal  46291  salunicl  46293  saluncl  46294  prsal  46295  salgenval  46298  intsaluni  46306  salgenn0  46308  salgencl  46309  sssalgen  46312  salgenss  46313  salgenuni  46314  issalgend  46315  dfsalgen2  46318  issalnnd  46322  meadjuni  46434  ismeannd  46444  omeunile  46482  caragenunicl  46501  isomennd  46508  issmflem  46704  onsetreclem1  49517