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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  unieqi  4879  unieqd  4880  uniintsn  4945  iununi  5059  treq  5219  eqsnuniex  5323  elvvuni  5728  unielrel  6276  unixp0  6286  unixpid  6287  limeq  6374  unizlim  6487  iotauni2  6510  opabiotafun  6965  uniexg  7757  onsucuni2  7845  onuninsuci  7851  orduninsuc  7854  undefval  8294  en1b  9052  fissorduni  9282  nnunifi  9283  fissuni  9346  infeq5i  9637  infeq5  9638  rnttrcl  9723  ttrclselem2  9727  trcl  9729  rankuni  9879  rankxplim3  9898  iunfictbso  10193  cflim2  10341  cfss  10343  cfslb  10344  fin2i  10373  fin1a2lem10  10487  fin1a2lem11  10488  fin1a2lem12  10489  itunisuc  10497  ituniiun  10500  hsmex  10510  dominf  10523  zornn0g  10583  dominfac  10658  wununi  10791  wunex2  10823  wuncval2  10832  incexclem  16005  mrcfval  17782  mrisval  17804  acsdrsel  18717  isacs4lem  18718  isacs5lem  18719  acsdrscl  18720  isps  18742  isdir  18772  sylow2a  19833  uniopn  23215  istopon  23230  eltg3  23280  tgdom  23296  indistopon  23319  cldval  23341  ntrfval  23342  clsfval  23343  mretopd  23410  neifval  23417  lpfval  23456  isperf  23469  tgrest  23477  ist0  23638  ist1  23639  ishaus  23640  iscnrm  23641  iscmp  23706  cmpcov  23707  cmpcovf  23709  cncmp  23710  fincmp  23711  cmpsublem  23717  cmpsub  23718  tgcmp  23719  cmpcld  23720  uncmp  23721  hauscmplem  23724  cmpfi  23726  isconn  23731  is1stc  23759  2ndc1stc  23769  2ndcsep  23778  isref  23828  isptfin  23835  islocfin  23836  comppfsc  23851  kgenval  23854  1stckgenlem  23872  txcmplem1  23960  txcmplem2  23961  kqval  24045  flffval  24308  fclsval  24327  fcfval  24352  alexsublem  24363  alexsubb  24365  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  ptcmplem2  24372  ptcmplem3  24373  ptcmplem5  24375  cnextval  24380  iscfilu  24606  icccmplem1  25142  icccmplem2  25143  bndth  25279  lebnumlem3  25284  om1val  25351  pi1val  25358  ovolicc2  25843  isplig  31078  hsupval  31936  acunirnmpt  33253  iscref  34476  crefi  34479  cmpcref  34482  pcmplfin  34492  sigaclcu  34749  prsiga  34763  sigaclci  34764  unelsiga  34766  sigagenval  34773  unelldsys  34791  sigapildsys  34795  ldgenpisyslem1  34796  rossros  34813  measvun  34842  ismbfm  34884  dya2iocuni  34915  oms0  34929  omssubadd  34932  carsgsigalem  34947  fiunelcarsg  34948  carsgclctunlem1  34949  carsgclctunlem2  34951  carsgclctunlem3  34952  carsgclctun  34953  pmeasmono  34956  pmeasadd  34957  fineqvnttrclselem2  35790  wevgblacfn  35890  kur14  35981  ispconn  35988  cvmscbv  36023  cvmsi  36030  cvmsval  36031  nnuni  36492  dfrdg2  36557  brbigcup  36660  dfbigcup2  36661  fobigcup  36662  brapply  36700  dfrdg4  36715  isfne  37127  fneval  37140  fnemeet1  37154  fnemeet2  37155  fnejoin1  37156  fnejoin2  37157  tailfval  37160  ordtoplem  37223  onsucsuccmpi  37231  limsucncmpi  37233  ordcmp  37235  ttctr  37281  ttcmin  37284  dfttc2g  37294  bj-ismoore  38026  dissneqlem  38263  finxpreclem3  38316  pibp19  38337  pibp21  38338  pibt2  38340  heicant  38573  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  mbfresfi  38584  cover2  38649  cover2g  38650  istotbnd3  38705  sstotbnd  38709  heiborlem1  38745  heiborlem6  38750  heiborlem8  38752  dmqseqim  39673  isnacs3  43720  nacsfix  43722  onsupnmax  44229  onov0suclim  44275  pwelg  44560  mnuprdlem1  45255  mnuprdlem2  45256  mnuunid  45260  mnurndlem1  45264  ismnushort  45284  csbfv12gALTVD  45880  stoweidlem35  47044  stoweidlem39  47048  stoweidlem50  47059  stoweidlem57  47066  issal  47323  salunicl  47325  saluncl  47326  prsal  47327  salgenval  47330  intsaluni  47338  salgenn0  47340  salgencl  47341  sssalgen  47344  salgenss  47345  salgenuni  47346  issalgend  47347  dfsalgen2  47350  issalnnd  47354  meadjuni  47466  ismeannd  47476  omeunile  47514  caragenunicl  47533  isomennd  47540  issmflem  47736  termco  50588  onsetreclem1  50797