Theorem unieq 4922

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 4053	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4921	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4054	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4921	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 4012	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1536  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  unieqi  4923  unieqd  4924  uniintsn  4989  iununi  5103  treq  5272  eqsnuniex  5366  elvvuni  5764  unielrel  6295  unixp0  6304  unixpid  6305  limeq  6397  unizlim  6508  iotauni2  6531  opabiotafun  6988  uniexg  7758  onsucuni2  7853  onuninsuci  7860  orduninsuc  7863  undefval  8299  en1b  9063  nnunifi  9324  fissuni  9394  infeq5i  9673  infeq5  9674  rnttrcl  9759  ttrclselem2  9763  trcl  9765  rankuni  9900  rankxplim3  9918  iunfictbso  10151  cflim2  10300  cfss  10302  cfslb  10303  fin2i  10332  fin1a2lem10  10446  fin1a2lem11  10447  fin1a2lem12  10448  itunisuc  10456  ituniiun  10459  hsmex  10469  dominf  10482  zornn0g  10542  dominfac  10610  wununi  10743  wunex2  10775  wuncval2  10784  incexclem  15868  mrcfval  17652  mrisval  17674  acsdrsel  18600  isacs4lem  18601  isacs5lem  18602  acsdrscl  18603  isps  18625  isdir  18655  sylow2a  19651  uniopn  22918  istopon  22933  eltg3  22984  tgdom  23000  indistopon  23023  cldval  23046  ntrfval  23047  clsfval  23048  mretopd  23115  neifval  23122  lpfval  23161  isperf  23174  tgrest  23182  ist0  23343  ist1  23344  ishaus  23345  iscnrm  23346  iscmp  23411  cmpcov  23412  cmpcovf  23414  cncmp  23415  fincmp  23416  cmpsublem  23422  cmpsub  23423  tgcmp  23424  cmpcld  23425  uncmp  23426  hauscmplem  23429  cmpfi  23431  isconn  23436  is1stc  23464  2ndc1stc  23474  2ndcsep  23482  isref  23532  isptfin  23539  islocfin  23540  comppfsc  23555  kgenval  23558  1stckgenlem  23576  txcmplem1  23664  txcmplem2  23665  kqval  23749  flffval  24012  fclsval  24031  fcfval  24056  alexsublem  24067  alexsubb  24069  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  ptcmplem2  24076  ptcmplem3  24077  ptcmplem5  24079  cnextval  24084  iscfilu  24312  icccmplem1  24857  icccmplem2  24858  bndth  25003  lebnumlem3  25008  om1val  25076  pi1val  25083  ovolicc2  25570  isplig  30504  hsupval  31362  acunirnmpt  32675  iscref  33804  crefi  33807  cmpcref  33810  pcmplfin  33820  sigaclcu  34097  prsiga  34111  sigaclci  34112  unelsiga  34114  sigagenval  34120  unelldsys  34138  sigapildsys  34142  ldgenpisyslem1  34143  rossros  34160  measvun  34189  ismbfm  34231  dya2iocuni  34264  oms0  34278  omssubadd  34281  carsgsigalem  34296  fiunelcarsg  34297  carsgclctunlem1  34298  carsgclctunlem2  34300  carsgclctunlem3  34301  carsgclctun  34302  pmeasmono  34305  pmeasadd  34306  wevgblacfn  35092  kur14  35200  ispconn  35207  cvmscbv  35242  cvmsi  35249  cvmsval  35250  nnuni  35706  dfrdg2  35776  brbigcup  35879  dfbigcup2  35880  fobigcup  35881  brapply  35919  dfrdg4  35932  isfne  36321  fneval  36334  fnemeet1  36348  fnemeet2  36349  fnejoin1  36350  fnejoin2  36351  tailfval  36354  ordtoplem  36417  onsucsuccmpi  36425  limsucncmpi  36427  ordcmp  36429  bj-ismoore  37087  dissneqlem  37322  finxpreclem3  37375  pibp19  37396  pibp21  37397  pibt2  37399  heicant  37641  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  cover2  37701  cover2g  37702  istotbnd3  37757  sstotbnd  37761  heiborlem1  37797  heiborlem6  37802  heiborlem8  37804  dmqseqim  38637  isnacs3  42697  nacsfix  42699  onsupnmax  43216  onov0suclim  43263  pwelg  43549  mnuprdlem1  44267  mnuprdlem2  44268  mnuunid  44272  mnurndlem1  44276  ismnushort  44296  csbfv12gALTVD  44896  stoweidlem35  45990  stoweidlem39  45994  stoweidlem50  46005  stoweidlem57  46012  issal  46269  salunicl  46271  saluncl  46272  prsal  46273  salgenval  46276  intsaluni  46284  salgenn0  46286  salgencl  46287  sssalgen  46290  salgenss  46291  salgenuni  46292  issalgend  46293  dfsalgen2  46296  issalnnd  46300  meadjuni  46412  ismeannd  46422  omeunile  46460  caragenunicl  46479  isomennd  46486  issmflem  46682  onsetreclem1  48935