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

Syntax hints:   → wi 4   = wceq 1540  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unieqi  4879  unieqd  4880  uniintsn  4945  iununi  5058  treq  5217  eqsnuniex  5311  elvvuni  5708  unielrel  6235  unixp0  6244  unixpid  6245  limeq  6332  unizlim  6445  iotauni2  6468  opabiotafun  6923  uniexg  7696  onsucuni2  7789  onuninsuci  7796  orduninsuc  7799  undefval  8232  en1b  8973  nnunifi  9214  fissuni  9284  infeq5i  9565  infeq5  9566  rnttrcl  9651  ttrclselem2  9655  trcl  9657  rankuni  9792  rankxplim3  9810  iunfictbso  10043  cflim2  10192  cfss  10194  cfslb  10195  fin2i  10224  fin1a2lem10  10338  fin1a2lem11  10339  fin1a2lem12  10340  itunisuc  10348  ituniiun  10351  hsmex  10361  dominf  10374  zornn0g  10434  dominfac  10502  wununi  10635  wunex2  10667  wuncval2  10676  incexclem  15778  mrcfval  17549  mrisval  17571  acsdrsel  18484  isacs4lem  18485  isacs5lem  18486  acsdrscl  18487  isps  18509  isdir  18539  sylow2a  19533  uniopn  22817  istopon  22832  eltg3  22882  tgdom  22898  indistopon  22921  cldval  22943  ntrfval  22944  clsfval  22945  mretopd  23012  neifval  23019  lpfval  23058  isperf  23071  tgrest  23079  ist0  23240  ist1  23241  ishaus  23242  iscnrm  23243  iscmp  23308  cmpcov  23309  cmpcovf  23311  cncmp  23312  fincmp  23313  cmpsublem  23319  cmpsub  23320  tgcmp  23321  cmpcld  23322  uncmp  23323  hauscmplem  23326  cmpfi  23328  isconn  23333  is1stc  23361  2ndc1stc  23371  2ndcsep  23379  isref  23429  isptfin  23436  islocfin  23437  comppfsc  23452  kgenval  23455  1stckgenlem  23473  txcmplem1  23561  txcmplem2  23562  kqval  23646  flffval  23909  fclsval  23928  fcfval  23953  alexsublem  23964  alexsubb  23966  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  alexsubALT  23971  ptcmplem2  23973  ptcmplem3  23974  ptcmplem5  23976  cnextval  23981  iscfilu  24208  icccmplem1  24744  icccmplem2  24745  bndth  24890  lebnumlem3  24895  om1val  24963  pi1val  24970  ovolicc2  25456  isplig  30455  hsupval  31313  acunirnmpt  32633  iscref  33827  crefi  33830  cmpcref  33833  pcmplfin  33843  sigaclcu  34100  prsiga  34114  sigaclci  34115  unelsiga  34117  sigagenval  34123  unelldsys  34141  sigapildsys  34145  ldgenpisyslem1  34146  rossros  34163  measvun  34192  ismbfm  34234  dya2iocuni  34267  oms0  34281  omssubadd  34284  carsgsigalem  34299  fiunelcarsg  34300  carsgclctunlem1  34301  carsgclctunlem2  34303  carsgclctunlem3  34304  carsgclctun  34305  pmeasmono  34308  pmeasadd  34309  wevgblacfn  35089  kur14  35196  ispconn  35203  cvmscbv  35238  cvmsi  35245  cvmsval  35246  nnuni  35707  dfrdg2  35776  brbigcup  35879  dfbigcup2  35880  fobigcup  35881  brapply  35919  dfrdg4  35932  isfne  36320  fneval  36333  fnemeet1  36347  fnemeet2  36348  fnejoin1  36349  fnejoin2  36350  tailfval  36353  ordtoplem  36416  onsucsuccmpi  36424  limsucncmpi  36426  ordcmp  36428  bj-ismoore  37086  dissneqlem  37321  finxpreclem3  37374  pibp19  37395  pibp21  37396  pibt2  37398  heicant  37642  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  mbfresfi  37653  cover2  37702  cover2g  37703  istotbnd3  37758  sstotbnd  37762  heiborlem1  37798  heiborlem6  37803  heiborlem8  37805  dmqseqim  38641  isnacs3  42691  nacsfix  42693  onsupnmax  43210  onov0suclim  43256  pwelg  43542  mnuprdlem1  44254  mnuprdlem2  44255  mnuunid  44259  mnurndlem1  44263  ismnushort  44283  csbfv12gALTVD  44881  stoweidlem35  46026  stoweidlem39  46030  stoweidlem50  46041  stoweidlem57  46048  issal  46305  salunicl  46307  saluncl  46308  prsal  46309  salgenval  46312  intsaluni  46320  salgenn0  46322  salgencl  46323  sssalgen  46326  salgenss  46327  salgenuni  46328  issalgend  46329  dfsalgen2  46332  issalnnd  46336  meadjuni  46448  ismeannd  46458  omeunile  46496  caragenunicl  46515  isomennd  46522  issmflem  46718  termco  49463  onsetreclem1  49687