Theorem unieq 4878

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  unieqi  4879  unieqd  4880  uniintsn  4945  iununi  5059  treq  5219  eqsnuniex  5326  elvvuni  5732  unielrel  6271  unixp0  6281  unixpid  6282  limeq  6369  unizlim  6482  iotauni2  6505  opabiotafun  6959  uniexg  7743  onsucuni2  7831  onuninsuci  7837  orduninsuc  7840  undefval  8276  en1b  9034  nnunifi  9264  fissuni  9327  infeq5i  9618  infeq5  9619  rnttrcl  9704  ttrclselem2  9708  trcl  9710  rankuni  9848  rankxplim3  9866  iunfictbso  10120  cflim2  10268  cfss  10270  cfslb  10271  fin2i  10300  fin1a2lem10  10414  fin1a2lem11  10415  fin1a2lem12  10416  itunisuc  10424  ituniiun  10427  hsmex  10437  dominf  10450  zornn0g  10510  dominfac  10585  wununi  10718  wunex2  10750  wuncval2  10759  incexclem  15928  mrcfval  17699  mrisval  17721  acsdrsel  18634  isacs4lem  18635  isacs5lem  18636  acsdrscl  18637  isps  18659  isdir  18689  sylow2a  19749  uniopn  23125  istopon  23140  eltg3  23190  tgdom  23206  indistopon  23229  cldval  23251  ntrfval  23252  clsfval  23253  mretopd  23320  neifval  23327  lpfval  23366  isperf  23379  tgrest  23387  ist0  23548  ist1  23549  ishaus  23550  iscnrm  23551  iscmp  23616  cmpcov  23617  cmpcovf  23619  cncmp  23620  fincmp  23621  cmpsublem  23627  cmpsub  23628  tgcmp  23629  cmpcld  23630  uncmp  23631  hauscmplem  23634  cmpfi  23636  isconn  23641  is1stc  23669  2ndc1stc  23679  2ndcsep  23688  isref  23738  isptfin  23745  islocfin  23746  comppfsc  23761  kgenval  23764  1stckgenlem  23782  txcmplem1  23870  txcmplem2  23871  kqval  23955  flffval  24218  fclsval  24237  fcfval  24262  alexsublem  24273  alexsubb  24275  alexsubALTlem2  24277  alexsubALTlem3  24278  alexsubALTlem4  24279  alexsubALT  24280  ptcmplem2  24282  ptcmplem3  24283  ptcmplem5  24285  cnextval  24290  iscfilu  24516  icccmplem1  25052  icccmplem2  25053  bndth  25189  lebnumlem3  25194  om1val  25261  pi1val  25268  ovolicc2  25753  isplig  30960  hsupval  31818  acunirnmpt  33135  iscref  34357  crefi  34360  cmpcref  34363  pcmplfin  34373  sigaclcu  34630  prsiga  34644  sigaclci  34645  unelsiga  34647  sigagenval  34654  unelldsys  34672  sigapildsys  34676  ldgenpisyslem1  34677  rossros  34694  measvun  34723  ismbfm  34765  dya2iocuni  34797  oms0  34811  omssubadd  34814  carsgsigalem  34829  fiunelcarsg  34830  carsgclctunlem1  34831  carsgclctunlem2  34833  carsgclctunlem3  34834  carsgclctun  34835  pmeasmono  34838  pmeasadd  34839  fissorduni  35597  fineqvnttrclselem2  35651  wevgblacfn  35711  kur14  35798  ispconn  35805  cvmscbv  35840  cvmsi  35847  cvmsval  35848  nnuni  36309  dfrdg2  36375  brbigcup  36478  dfbigcup2  36479  fobigcup  36480  brapply  36518  dfrdg4  36533  isfne  36961  fneval  36974  fnemeet1  36988  fnemeet2  36989  fnejoin1  36990  fnejoin2  36991  tailfval  36994  ordtoplem  37057  onsucsuccmpi  37065  limsucncmpi  37067  ordcmp  37069  ttctr  37115  ttcmin  37118  dfttc2g  37128  bj-ismoore  37858  dissneqlem  38097  finxpreclem3  38150  pibp19  38171  pibp21  38172  pibt2  38174  heicant  38407  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  mbfresfi  38418  cover2  38468  cover2g  38469  istotbnd3  38524  sstotbnd  38528  heiborlem1  38564  heiborlem6  38569  heiborlem8  38571  dmqseqim  39492  isnacs3  43558  nacsfix  43560  onsupnmax  44072  onov0suclim  44118  pwelg  44403  mnuprdlem1  45099  mnuprdlem2  45100  mnuunid  45104  mnurndlem1  45108  ismnushort  45128  csbfv12gALTVD  45724  stoweidlem35  46866  stoweidlem39  46870  stoweidlem50  46881  stoweidlem57  46888  issal  47145  salunicl  47147  saluncl  47148  prsal  47149  salgenval  47152  intsaluni  47160  salgenn0  47162  salgencl  47163  sssalgen  47166  salgenss  47167  salgenuni  47168  issalgend  47169  dfsalgen2  47172  issalnnd  47176  meadjuni  47288  ismeannd  47298  omeunile  47336  caragenunicl  47355  isomennd  47362  issmflem  47558  termco  50410  onsetreclem1  50634