Theorem unieq 4882

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 4005	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4881	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4006	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4881	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3964	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unieqi  4883  unieqd  4884  uniintsn  4949  iununi  5063  treq  5222  eqsnuniex  5316  elvvuni  5715  unielrel  6247  unixp0  6256  unixpid  6257  limeq  6344  unizlim  6457  iotauni2  6480  opabiotafun  6941  uniexg  7716  onsucuni2  7809  onuninsuci  7816  orduninsuc  7819  undefval  8255  en1b  8996  nnunifi  9238  fissuni  9308  infeq5i  9589  infeq5  9590  rnttrcl  9675  ttrclselem2  9679  trcl  9681  rankuni  9816  rankxplim3  9834  iunfictbso  10067  cflim2  10216  cfss  10218  cfslb  10219  fin2i  10248  fin1a2lem10  10362  fin1a2lem11  10363  fin1a2lem12  10364  itunisuc  10372  ituniiun  10375  hsmex  10385  dominf  10398  zornn0g  10458  dominfac  10526  wununi  10659  wunex2  10691  wuncval2  10700  incexclem  15802  mrcfval  17569  mrisval  17591  acsdrsel  18502  isacs4lem  18503  isacs5lem  18504  acsdrscl  18505  isps  18527  isdir  18557  sylow2a  19549  uniopn  22784  istopon  22799  eltg3  22849  tgdom  22865  indistopon  22888  cldval  22910  ntrfval  22911  clsfval  22912  mretopd  22979  neifval  22986  lpfval  23025  isperf  23038  tgrest  23046  ist0  23207  ist1  23208  ishaus  23209  iscnrm  23210  iscmp  23275  cmpcov  23276  cmpcovf  23278  cncmp  23279  fincmp  23280  cmpsublem  23286  cmpsub  23287  tgcmp  23288  cmpcld  23289  uncmp  23290  hauscmplem  23293  cmpfi  23295  isconn  23300  is1stc  23328  2ndc1stc  23338  2ndcsep  23346  isref  23396  isptfin  23403  islocfin  23404  comppfsc  23419  kgenval  23422  1stckgenlem  23440  txcmplem1  23528  txcmplem2  23529  kqval  23613  flffval  23876  fclsval  23895  fcfval  23920  alexsublem  23931  alexsubb  23933  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem2  23940  ptcmplem3  23941  ptcmplem5  23943  cnextval  23948  iscfilu  24175  icccmplem1  24711  icccmplem2  24712  bndth  24857  lebnumlem3  24862  om1val  24930  pi1val  24937  ovolicc2  25423  isplig  30405  hsupval  31263  acunirnmpt  32583  iscref  33834  crefi  33837  cmpcref  33840  pcmplfin  33850  sigaclcu  34107  prsiga  34121  sigaclci  34122  unelsiga  34124  sigagenval  34130  unelldsys  34148  sigapildsys  34152  ldgenpisyslem1  34153  rossros  34170  measvun  34199  ismbfm  34241  dya2iocuni  34274  oms0  34288  omssubadd  34291  carsgsigalem  34306  fiunelcarsg  34307  carsgclctunlem1  34308  carsgclctunlem2  34310  carsgclctunlem3  34311  carsgclctun  34312  pmeasmono  34315  pmeasadd  34316  wevgblacfn  35096  kur14  35203  ispconn  35210  cvmscbv  35245  cvmsi  35252  cvmsval  35253  nnuni  35714  dfrdg2  35783  brbigcup  35886  dfbigcup2  35887  fobigcup  35888  brapply  35926  dfrdg4  35939  isfne  36327  fneval  36340  fnemeet1  36354  fnemeet2  36355  fnejoin1  36356  fnejoin2  36357  tailfval  36360  ordtoplem  36423  onsucsuccmpi  36431  limsucncmpi  36433  ordcmp  36435  bj-ismoore  37093  dissneqlem  37328  finxpreclem3  37381  pibp19  37402  pibp21  37403  pibt2  37405  heicant  37649  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  cover2  37709  cover2g  37710  istotbnd3  37765  sstotbnd  37769  heiborlem1  37805  heiborlem6  37810  heiborlem8  37812  dmqseqim  38648  isnacs3  42698  nacsfix  42700  onsupnmax  43217  onov0suclim  43263  pwelg  43549  mnuprdlem1  44261  mnuprdlem2  44262  mnuunid  44266  mnurndlem1  44270  ismnushort  44290  csbfv12gALTVD  44888  stoweidlem35  46033  stoweidlem39  46037  stoweidlem50  46048  stoweidlem57  46055  issal  46312  salunicl  46314  saluncl  46315  prsal  46316  salgenval  46319  intsaluni  46327  salgenn0  46329  salgencl  46330  sssalgen  46333  salgenss  46334  salgenuni  46335  issalgend  46336  dfsalgen2  46339  issalnnd  46343  meadjuni  46455  ismeannd  46465  omeunile  46503  caragenunicl  46522  isomennd  46529  issmflem  46725  termco  49470  onsetreclem1  49694