Theorem unieq 4872

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 3990	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4871	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3991	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4871	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3949	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-uni 4862

This theorem is referenced by:  unieqi  4873  unieqd  4874  uniintsn  4938  iununi  5052  treq  5210  eqsnuniex  5304  elvvuni  5699  unielrel  6230  unixp0  6239  unixpid  6240  limeq  6327  unizlim  6439  iotauni2  6462  opabiotafun  6912  uniexg  7683  onsucuni2  7774  onuninsuci  7780  orduninsuc  7783  undefval  8216  en1b  8960  nnunifi  9189  fissuni  9255  infeq5i  9543  infeq5  9544  rnttrcl  9629  ttrclselem2  9633  trcl  9635  rankuni  9773  rankxplim3  9791  iunfictbso  10022  cflim2  10171  cfss  10173  cfslb  10174  fin2i  10203  fin1a2lem10  10317  fin1a2lem11  10318  fin1a2lem12  10319  itunisuc  10327  ituniiun  10330  hsmex  10340  dominf  10353  zornn0g  10413  dominfac  10482  wununi  10615  wunex2  10647  wuncval2  10656  incexclem  15757  mrcfval  17529  mrisval  17551  acsdrsel  18464  isacs4lem  18465  isacs5lem  18466  acsdrscl  18467  isps  18489  isdir  18519  sylow2a  19546  uniopn  22839  istopon  22854  eltg3  22904  tgdom  22920  indistopon  22943  cldval  22965  ntrfval  22966  clsfval  22967  mretopd  23034  neifval  23041  lpfval  23080  isperf  23093  tgrest  23101  ist0  23262  ist1  23263  ishaus  23264  iscnrm  23265  iscmp  23330  cmpcov  23331  cmpcovf  23333  cncmp  23334  fincmp  23335  cmpsublem  23341  cmpsub  23342  tgcmp  23343  cmpcld  23344  uncmp  23345  hauscmplem  23348  cmpfi  23350  isconn  23355  is1stc  23383  2ndc1stc  23393  2ndcsep  23401  isref  23451  isptfin  23458  islocfin  23459  comppfsc  23474  kgenval  23477  1stckgenlem  23495  txcmplem1  23583  txcmplem2  23584  kqval  23668  flffval  23931  fclsval  23950  fcfval  23975  alexsublem  23986  alexsubb  23988  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  alexsubALT  23993  ptcmplem2  23995  ptcmplem3  23996  ptcmplem5  23998  cnextval  24003  iscfilu  24229  icccmplem1  24765  icccmplem2  24766  bndth  24911  lebnumlem3  24916  om1val  24984  pi1val  24991  ovolicc2  25477  isplig  30500  hsupval  31358  acunirnmpt  32686  iscref  33950  crefi  33953  cmpcref  33956  pcmplfin  33966  sigaclcu  34223  prsiga  34237  sigaclci  34238  unelsiga  34240  sigagenval  34246  unelldsys  34264  sigapildsys  34268  ldgenpisyslem1  34269  rossros  34286  measvun  34315  ismbfm  34357  dya2iocuni  34389  oms0  34403  omssubadd  34406  carsgsigalem  34421  fiunelcarsg  34422  carsgclctunlem1  34423  carsgclctunlem2  34425  carsgclctunlem3  34426  carsgclctun  34427  pmeasmono  34430  pmeasadd  34431  fissorduni  35195  fineqvnttrclselem2  35227  wevgblacfn  35252  kur14  35359  ispconn  35366  cvmscbv  35401  cvmsi  35408  cvmsval  35409  nnuni  35870  dfrdg2  35936  brbigcup  36039  dfbigcup2  36040  fobigcup  36041  brapply  36079  dfrdg4  36094  isfne  36482  fneval  36495  fnemeet1  36509  fnemeet2  36510  fnejoin1  36511  fnejoin2  36512  tailfval  36515  ordtoplem  36578  onsucsuccmpi  36586  limsucncmpi  36588  ordcmp  36590  bj-ismoore  37249  dissneqlem  37484  finxpreclem3  37537  pibp19  37558  pibp21  37559  pibt2  37561  heicant  37795  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  mbfresfi  37806  cover2  37855  cover2g  37856  istotbnd3  37911  sstotbnd  37915  heiborlem1  37951  heiborlem6  37956  heiborlem8  37958  dmqseqim  38854  isnacs3  42894  nacsfix  42896  onsupnmax  43412  onov0suclim  43458  pwelg  43743  mnuprdlem1  44455  mnuprdlem2  44456  mnuunid  44460  mnurndlem1  44464  ismnushort  44484  csbfv12gALTVD  45081  stoweidlem35  46221  stoweidlem39  46225  stoweidlem50  46236  stoweidlem57  46243  issal  46500  salunicl  46502  saluncl  46503  prsal  46504  salgenval  46507  intsaluni  46515  salgenn0  46517  salgencl  46518  sssalgen  46521  salgenss  46522  salgenuni  46523  issalgend  46524  dfsalgen2  46527  issalnnd  46531  meadjuni  46643  ismeannd  46653  omeunile  46691  caragenunicl  46710  isomennd  46717  issmflem  46913  termco  49668  onsetreclem1  49892