Theorem unieq 4885

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 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4884	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3997	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4884	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3955	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875

This theorem is used by:  unieqi  4886  unieqd  4887  uniintsn  4952  iununi  5067  treq  5227  eqsnuniex  5334  elvvuni  5740  unielrel  6278  unixp0  6288  unixpid  6289  limeq  6376  unizlim  6489  iotauni2  6512  opabiotafun  6965  uniexg  7748  onsucuni2  7836  onuninsuci  7842  orduninsuc  7845  undefval  8279  en1b  9028  nnunifi  9258  fissuni  9321  infeq5i  9612  infeq5  9613  rnttrcl  9698  ttrclselem2  9702  trcl  9704  rankuni  9842  rankxplim3  9860  iunfictbso  10114  cflim2  10262  cfss  10264  cfslb  10265  fin2i  10294  fin1a2lem10  10408  fin1a2lem11  10409  fin1a2lem12  10410  itunisuc  10418  ituniiun  10421  hsmex  10431  dominf  10444  zornn0g  10504  dominfac  10575  wununi  10708  wunex2  10740  wuncval2  10749  incexclem  15915  mrcfval  17688  mrisval  17710  acsdrsel  18623  isacs4lem  18624  isacs5lem  18625  acsdrscl  18626  isps  18648  isdir  18678  sylow2a  19735  uniopn  23106  istopon  23121  eltg3  23171  tgdom  23187  indistopon  23210  cldval  23232  ntrfval  23233  clsfval  23234  mretopd  23301  neifval  23308  lpfval  23347  isperf  23360  tgrest  23368  ist0  23529  ist1  23530  ishaus  23531  iscnrm  23532  iscmp  23597  cmpcov  23598  cmpcovf  23600  cncmp  23601  fincmp  23602  cmpsublem  23608  cmpsub  23609  tgcmp  23610  cmpcld  23611  uncmp  23612  hauscmplem  23615  cmpfi  23617  isconn  23622  is1stc  23650  2ndc1stc  23660  2ndcsep  23669  isref  23719  isptfin  23726  islocfin  23727  comppfsc  23742  kgenval  23745  1stckgenlem  23763  txcmplem1  23851  txcmplem2  23852  kqval  23936  flffval  24199  fclsval  24218  fcfval  24243  alexsublem  24254  alexsubb  24256  alexsubALTlem2  24258  alexsubALTlem3  24259  alexsubALTlem4  24260  alexsubALT  24261  ptcmplem2  24263  ptcmplem3  24264  ptcmplem5  24266  cnextval  24271  iscfilu  24497  icccmplem1  25033  icccmplem2  25034  bndth  25170  lebnumlem3  25175  om1val  25242  pi1val  25249  ovolicc2  25734  isplig  30901  hsupval  31759  acunirnmpt  33077  iscref  34300  crefi  34303  cmpcref  34306  pcmplfin  34316  sigaclcu  34573  prsiga  34587  sigaclci  34588  unelsiga  34590  sigagenval  34597  unelldsys  34615  sigapildsys  34619  ldgenpisyslem1  34620  rossros  34637  measvun  34666  ismbfm  34708  dya2iocuni  34740  oms0  34754  omssubadd  34757  carsgsigalem  34772  fiunelcarsg  34773  carsgclctunlem1  34774  carsgclctunlem2  34776  carsgclctunlem3  34777  carsgclctun  34778  pmeasmono  34781  pmeasadd  34782  fissorduni  35540  fineqvnttrclselem2  35594  wevgblacfn  35654  kur14  35747  ispconn  35754  cvmscbv  35789  cvmsi  35796  cvmsval  35797  nnuni  36258  dfrdg2  36324  brbigcup  36427  dfbigcup2  36428  fobigcup  36429  brapply  36467  dfrdg4  36482  isfne  36909  fneval  36922  fnemeet1  36936  fnemeet2  36937  fnejoin1  36938  fnejoin2  36939  tailfval  36942  ordtoplem  37005  onsucsuccmpi  37013  limsucncmpi  37015  ordcmp  37017  ttctr  37063  ttcmin  37066  dfttc2g  37076  bj-ismoore  37806  dissneqlem  38045  finxpreclem3  38098  pibp19  38119  pibp21  38120  pibt2  38122  heicant  38365  ovoliunnfl  38372  voliunnfl  38374  volsupnfl  38375  mbfresfi  38376  cover2  38426  cover2g  38427  istotbnd3  38482  sstotbnd  38486  heiborlem1  38522  heiborlem6  38527  heiborlem8  38529  dmqseqim  39450  isnacs3  43501  nacsfix  43503  onsupnmax  44015  onov0suclim  44061  pwelg  44346  mnuprdlem1  45042  mnuprdlem2  45043  mnuunid  45047  mnurndlem1  45051  ismnushort  45071  csbfv12gALTVD  45667  stoweidlem35  46809  stoweidlem39  46813  stoweidlem50  46824  stoweidlem57  46831  issal  47088  salunicl  47090  saluncl  47091  prsal  47092  salgenval  47095  intsaluni  47103  salgenn0  47105  salgencl  47106  sssalgen  47109  salgenss  47110  salgenuni  47111  issalgend  47112  dfsalgen2  47115  issalnnd  47119  meadjuni  47231  ismeannd  47241  omeunile  47279  caragenunicl  47298  isomennd  47305  issmflem  47501  termco  50318  onsetreclem1  50542