Theorem unieq 4880

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 3970	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4879	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3971	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4879	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3929	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∪ cuni 4869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-uni 4870

This theorem is used by:  unieqi  4881  unieqd  4882  uniintsn  4947  iununi  5061  treq  5221  eqsnuniex  5326  elvvuni  5732  unielrel  6282  unixp0  6292  unixpid  6293  limeq  6380  unizlim  6493  iotauni2  6516  opabiotafun  6973  uniexg  7764  onsucuni2  7852  onuninsuci  7858  orduninsuc  7861  undefval  8305  en1b  9063  fissorduni  9293  nnunifi  9294  fissuni  9357  infeq5i  9647  infeq5  9648  rnttrcl  9733  ttrclselem2  9737  trcl  9739  rankuni  9889  rankxplim3  9908  iunfictbso  10203  cflim2  10351  cfss  10353  cfslb  10354  fin2i  10383  fin1a2lem10  10497  fin1a2lem11  10498  fin1a2lem12  10499  itunisuc  10507  ituniiun  10510  hsmex  10520  dominf  10533  zornn0g  10593  dominfac  10668  wununi  10801  wunex2  10833  wuncval2  10842  incexclem  16017  mrcfval  17794  mrisval  17816  acsdrsel  18729  isacs4lem  18730  isacs5lem  18731  acsdrscl  18732  isps  18754  isdir  18784  sylow2a  19845  uniopn  23227  istopon  23242  eltg3  23292  tgdom  23308  indistopon  23331  cldval  23353  ntrfval  23354  clsfval  23355  mretopd  23422  neifval  23429  lpfval  23468  isperf  23481  tgrest  23489  ist0  23650  ist1  23651  ishaus  23652  iscnrm  23653  iscmp  23718  cmpcov  23719  cmpcovf  23721  cncmp  23722  fincmp  23723  cmpsublem  23729  cmpsub  23730  tgcmp  23731  cmpcld  23732  uncmp  23733  hauscmplem  23736  cmpfi  23738  isconn  23743  is1stc  23771  2ndc1stc  23781  2ndcsep  23790  isref  23840  isptfin  23847  islocfin  23848  comppfsc  23863  kgenval  23866  1stckgenlem  23884  txcmplem1  23972  txcmplem2  23973  kqval  24057  flffval  24320  fclsval  24339  fcfval  24364  alexsublem  24375  alexsubb  24377  alexsubALTlem2  24379  alexsubALTlem3  24380  alexsubALTlem4  24381  alexsubALT  24382  ptcmplem2  24384  ptcmplem3  24385  ptcmplem5  24387  cnextval  24392  iscfilu  24618  icccmplem1  25154  icccmplem2  25155  bndth  25291  lebnumlem3  25296  om1val  25363  pi1val  25370  ovolicc2  25855  isplig  31090  hsupval  31948  acunirnmpt  33307  iscref  34529  crefi  34532  cmpcref  34535  pcmplfin  34545  sigaclcu  34802  prsiga  34816  sigaclci  34817  unelsiga  34819  sigagenval  34826  unelldsys  34844  sigapildsys  34848  ldgenpisyslem1  34849  rossros  34866  measvun  34895  ismbfm  34937  dya2iocuni  34968  oms0  34982  omssubadd  34985  carsgsigalem  35000  fiunelcarsg  35001  carsgclctunlem1  35002  carsgclctunlem2  35004  carsgclctunlem3  35005  carsgclctun  35006  pmeasmono  35009  pmeasadd  35010  fineqvnttrclselem2  35861  wevgblacfn  35993  kur14  36102  ispconn  36109  cvmscbv  36144  cvmsi  36151  cvmsval  36152  nnuni  36619  dfrdg2  36684  brbigcup  36787  dfbigcup2  36788  fobigcup  36789  brapply  36827  dfrdg4  36842  isfne  37254  fneval  37267  fnemeet1  37281  fnemeet2  37282  fnejoin1  37283  fnejoin2  37284  tailfval  37287  ordtoplem  37350  onsucsuccmpi  37358  limsucncmpi  37360  ordcmp  37362  ttctr  37408  ttcmin  37411  dfttc2g  37421  bj-ismoore  38165  dissneqlem  38403  finxpreclem3  38456  pibp19  38477  pibp21  38478  pibt2  38480  heicant  38713  ovoliunnfl  38720  voliunnfl  38722  volsupnfl  38723  mbfresfi  38724  cover2  38789  cover2g  38790  istotbnd3  38845  sstotbnd  38849  heiborlem1  38885  heiborlem6  38890  heiborlem8  38892  dmqseqim  39813  isnacs3  43861  nacsfix  43863  onsupnmax  44370  onov0suclim  44416  pwelg  44701  mnuprdlem1  45396  mnuprdlem2  45397  mnuunid  45401  mnurndlem1  45405  ismnushort  45425  csbfv12gALTVD  46020  stoweidlem35  47184  stoweidlem39  47188  stoweidlem50  47199  stoweidlem57  47206  issal  47463  salunicl  47465  saluncl  47466  prsal  47467  salgenval  47470  intsaluni  47478  salgenn0  47480  salgencl  47481  sssalgen  47484  salgenss  47485  salgenuni  47486  issalgend  47487  dfsalgen2  47490  issalnnd  47494  meadjuni  47606  ismeannd  47616  omeunile  47654  caragenunicl  47673  isomennd  47680  issmflem  47876  termco  50755  onsetreclem1  51012