Theorem unieq 4887

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 4003	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4886	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4004	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4886	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3962	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1567  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877

This theorem is referenced by:  unieqi  4888  unieqd  4889  uniintsn  4954  iununi  5069  treq  5229  eqsnuniex  5333  elvvuni  5739  unielrel  6276  unixp0  6285  unixpid  6286  limeq  6373  unizlim  6486  iotauni2  6509  opabiotafun  6962  uniexg  7739  onsucuni2  7830  onuninsuci  7836  orduninsuc  7839  undefval  8273  en1b  9022  nnunifi  9251  fissuni  9314  infeq5i  9605  infeq5  9606  rnttrcl  9691  ttrclselem2  9695  trcl  9697  rankuni  9835  rankxplim3  9853  iunfictbso  10098  cflim2  10247  cfss  10249  cfslb  10250  fin2i  10279  fin1a2lem10  10393  fin1a2lem11  10394  fin1a2lem12  10395  itunisuc  10403  ituniiun  10406  hsmex  10416  dominf  10429  zornn0g  10489  dominfac  10558  wununi  10691  wunex2  10723  wuncval2  10732  incexclem  15890  mrcfval  17664  mrisval  17686  acsdrsel  18599  isacs4lem  18600  isacs5lem  18601  acsdrscl  18602  isps  18624  isdir  18654  sylow2a  19689  uniopn  23023  istopon  23038  eltg3  23088  tgdom  23104  indistopon  23127  cldval  23149  ntrfval  23150  clsfval  23151  mretopd  23218  neifval  23225  lpfval  23264  isperf  23277  tgrest  23285  ist0  23446  ist1  23447  ishaus  23448  iscnrm  23449  iscmp  23514  cmpcov  23515  cmpcovf  23517  cncmp  23518  fincmp  23519  cmpsublem  23525  cmpsub  23526  tgcmp  23527  cmpcld  23528  uncmp  23529  hauscmplem  23532  cmpfi  23534  isconn  23539  is1stc  23567  2ndc1stc  23577  2ndcsep  23585  isref  23635  isptfin  23642  islocfin  23643  comppfsc  23658  kgenval  23661  1stckgenlem  23679  txcmplem1  23767  txcmplem2  23768  kqval  23852  flffval  24115  fclsval  24134  fcfval  24159  alexsublem  24170  alexsubb  24172  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  alexsubALT  24177  ptcmplem2  24179  ptcmplem3  24180  ptcmplem5  24182  cnextval  24187  iscfilu  24413  icccmplem1  24949  icccmplem2  24950  bndth  25086  lebnumlem3  25091  om1val  25158  pi1val  25165  ovolicc2  25650  isplig  30769  hsupval  31627  acunirnmpt  32945  iscref  34179  crefi  34182  cmpcref  34185  pcmplfin  34195  sigaclcu  34452  prsiga  34466  sigaclci  34467  unelsiga  34469  sigagenval  34475  unelldsys  34493  sigapildsys  34497  ldgenpisyslem1  34498  rossros  34515  measvun  34544  ismbfm  34586  dya2iocuni  34618  oms0  34632  omssubadd  34635  carsgsigalem  34650  fiunelcarsg  34651  carsgclctunlem1  34652  carsgclctunlem2  34654  carsgclctunlem3  34655  carsgclctun  34656  pmeasmono  34659  pmeasadd  34660  fissorduni  35423  fineqvnttrclselem2  35458  wevgblacfn  35494  kur14  35607  ispconn  35614  cvmscbv  35649  cvmsi  35656  cvmsval  35657  nnuni  36118  dfrdg2  36184  brbigcup  36287  dfbigcup2  36288  fobigcup  36289  brapply  36327  dfrdg4  36342  isfne  36739  fneval  36752  fnemeet1  36766  fnemeet2  36767  fnejoin1  36768  fnejoin2  36769  tailfval  36772  ordtoplem  36835  onsucsuccmpi  36843  limsucncmpi  36845  ordcmp  36847  ttctr  36893  ttcmin  36896  dfttc2g  36906  bj-ismoore  37635  dissneqlem  37874  finxpreclem3  37927  pibp19  37948  pibp21  37949  pibt2  37951  heicant  38194  ovoliunnfl  38201  voliunnfl  38203  volsupnfl  38204  mbfresfi  38205  cover2  38254  cover2g  38255  istotbnd3  38310  sstotbnd  38314  heiborlem1  38350  heiborlem6  38355  heiborlem8  38357  dmqseqim  39280  isnacs3  43333  nacsfix  43335  onsupnmax  43847  onov0suclim  43893  pwelg  44178  mnuprdlem1  44874  mnuprdlem2  44875  mnuunid  44879  mnurndlem1  44883  ismnushort  44903  csbfv12gALTVD  45499  stoweidlem35  46641  stoweidlem39  46645  stoweidlem50  46656  stoweidlem57  46663  issal  46920  salunicl  46922  saluncl  46923  prsal  46924  salgenval  46927  intsaluni  46935  salgenn0  46937  salgencl  46938  sssalgen  46941  salgenss  46942  salgenuni  46943  issalgend  46944  dfsalgen2  46947  issalnnd  46951  meadjuni  47063  ismeannd  47073  omeunile  47111  caragenunicl  47130  isomennd  47137  issmflem  47333  termco  50144  onsetreclem1  50368