Theorem unieq 4876

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 3994	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4875	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4875	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3953	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unieqi  4877  unieqd  4878  uniintsn  4942  iununi  5056  treq  5214  eqsnuniex  5308  elvvuni  5709  unielrel  6240  unixp0  6249  unixpid  6250  limeq  6337  unizlim  6449  iotauni2  6472  opabiotafun  6922  uniexg  7695  onsucuni2  7786  onuninsuci  7792  orduninsuc  7795  undefval  8228  en1b  8974  nnunifi  9203  fissuni  9269  infeq5i  9557  infeq5  9558  rnttrcl  9643  ttrclselem2  9647  trcl  9649  rankuni  9787  rankxplim3  9805  iunfictbso  10036  cflim2  10185  cfss  10187  cfslb  10188  fin2i  10217  fin1a2lem10  10331  fin1a2lem11  10332  fin1a2lem12  10333  itunisuc  10341  ituniiun  10344  hsmex  10354  dominf  10367  zornn0g  10427  dominfac  10496  wununi  10629  wunex2  10661  wuncval2  10670  incexclem  15771  mrcfval  17543  mrisval  17565  acsdrsel  18478  isacs4lem  18479  isacs5lem  18480  acsdrscl  18481  isps  18503  isdir  18533  sylow2a  19560  uniopn  22853  istopon  22868  eltg3  22918  tgdom  22934  indistopon  22957  cldval  22979  ntrfval  22980  clsfval  22981  mretopd  23048  neifval  23055  lpfval  23094  isperf  23107  tgrest  23115  ist0  23276  ist1  23277  ishaus  23278  iscnrm  23279  iscmp  23344  cmpcov  23345  cmpcovf  23347  cncmp  23348  fincmp  23349  cmpsublem  23355  cmpsub  23356  tgcmp  23357  cmpcld  23358  uncmp  23359  hauscmplem  23362  cmpfi  23364  isconn  23369  is1stc  23397  2ndc1stc  23407  2ndcsep  23415  isref  23465  isptfin  23472  islocfin  23473  comppfsc  23488  kgenval  23491  1stckgenlem  23509  txcmplem1  23597  txcmplem2  23598  kqval  23682  flffval  23945  fclsval  23964  fcfval  23989  alexsublem  24000  alexsubb  24002  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  ptcmplem2  24009  ptcmplem3  24010  ptcmplem5  24012  cnextval  24017  iscfilu  24243  icccmplem1  24779  icccmplem2  24780  bndth  24925  lebnumlem3  24930  om1val  24998  pi1val  25005  ovolicc2  25491  isplig  30564  hsupval  31422  acunirnmpt  32749  iscref  34022  crefi  34025  cmpcref  34028  pcmplfin  34038  sigaclcu  34295  prsiga  34309  sigaclci  34310  unelsiga  34312  sigagenval  34318  unelldsys  34336  sigapildsys  34340  ldgenpisyslem1  34341  rossros  34358  measvun  34387  ismbfm  34429  dya2iocuni  34461  oms0  34475  omssubadd  34478  carsgsigalem  34493  fiunelcarsg  34494  carsgclctunlem1  34495  carsgclctunlem2  34497  carsgclctunlem3  34498  carsgclctun  34499  pmeasmono  34502  pmeasadd  34503  fissorduni  35267  fineqvnttrclselem2  35300  wevgblacfn  35325  kur14  35432  ispconn  35439  cvmscbv  35474  cvmsi  35481  cvmsval  35482  nnuni  35943  dfrdg2  36009  brbigcup  36112  dfbigcup2  36113  fobigcup  36114  brapply  36152  dfrdg4  36167  isfne  36555  fneval  36568  fnemeet1  36582  fnemeet2  36583  fnejoin1  36584  fnejoin2  36585  tailfval  36588  ordtoplem  36651  onsucsuccmpi  36659  limsucncmpi  36661  ordcmp  36663  bj-ismoore  37358  dissneqlem  37595  finxpreclem3  37648  pibp19  37669  pibp21  37670  pibt2  37672  heicant  37906  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  mbfresfi  37917  cover2  37966  cover2g  37967  istotbnd3  38022  sstotbnd  38026  heiborlem1  38062  heiborlem6  38067  heiborlem8  38069  dmqseqim  38992  isnacs3  43067  nacsfix  43069  onsupnmax  43585  onov0suclim  43631  pwelg  43916  mnuprdlem1  44628  mnuprdlem2  44629  mnuunid  44633  mnurndlem1  44637  ismnushort  44657  csbfv12gALTVD  45254  stoweidlem35  46393  stoweidlem39  46397  stoweidlem50  46408  stoweidlem57  46415  issal  46672  salunicl  46674  saluncl  46675  prsal  46676  salgenval  46679  intsaluni  46687  salgenn0  46689  salgencl  46690  sssalgen  46693  salgenss  46694  salgenuni  46695  issalgend  46696  dfsalgen2  46699  issalnnd  46703  meadjuni  46815  ismeannd  46825  omeunile  46863  caragenunicl  46882  isomennd  46889  issmflem  47085  termco  49840  onsetreclem1  50064