Theorem unieq 4850

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 3977	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4849	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3978	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4849	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3938	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1539  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  unieqi  4852  unieqd  4853  uniintsn  4918  iununi  5028  treq  5197  eqsnuniex  5283  elvvuni  5663  unielrel  6177  unixp0  6186  unixpid  6187  limeq  6278  unizlim  6383  opabiotafun  6849  uniexg  7593  onsucuni2  7681  onuninsuci  7687  orduninsuc  7690  undefval  8092  en1b  8813  en1bOLD  8814  nnunifi  9065  fissuni  9124  infeq5i  9394  infeq5  9395  rnttrcl  9480  ttrclselem2  9484  trcl  9486  rankuni  9621  rankxplim3  9639  iunfictbso  9870  cflim2  10019  cfss  10021  cfslb  10022  fin2i  10051  fin1a2lem10  10165  fin1a2lem11  10166  fin1a2lem12  10167  itunisuc  10175  ituniiun  10178  hsmex  10188  dominf  10201  zornn0g  10261  dominfac  10329  wununi  10462  wunex2  10494  wuncval2  10503  incexclem  15548  mrcfval  17317  mrisval  17339  acsdrsel  18261  isacs4lem  18262  isacs5lem  18263  acsdrscl  18264  isps  18286  isdir  18316  sylow2a  19224  uniopn  22046  istopon  22061  eltg3  22112  tgdom  22128  indistopon  22151  cldval  22174  ntrfval  22175  clsfval  22176  mretopd  22243  neifval  22250  lpfval  22289  isperf  22302  tgrest  22310  ist0  22471  ist1  22472  ishaus  22473  iscnrm  22474  iscmp  22539  cmpcov  22540  cmpcovf  22542  cncmp  22543  fincmp  22544  cmpsublem  22550  cmpsub  22551  tgcmp  22552  cmpcld  22553  uncmp  22554  hauscmplem  22557  cmpfi  22559  isconn  22564  is1stc  22592  2ndc1stc  22602  2ndcsep  22610  isref  22660  isptfin  22667  islocfin  22668  comppfsc  22683  kgenval  22686  1stckgenlem  22704  txcmplem1  22792  txcmplem2  22793  kqval  22877  flffval  23140  fclsval  23159  fcfval  23184  alexsublem  23195  alexsubb  23197  alexsubALTlem2  23199  alexsubALTlem3  23200  alexsubALTlem4  23201  alexsubALT  23202  ptcmplem2  23204  ptcmplem3  23205  ptcmplem5  23207  cnextval  23212  iscfilu  23440  icccmplem1  23985  icccmplem2  23986  bndth  24121  lebnumlem3  24126  om1val  24193  pi1val  24200  ovolicc2  24686  isplig  28838  hsupval  29696  acunirnmpt  30996  iscref  31794  crefi  31797  cmpcref  31800  pcmplfin  31810  sigaclcu  32085  prsiga  32099  sigaclci  32100  unelsiga  32102  sigagenval  32108  unelldsys  32126  sigapildsys  32130  ldgenpisyslem1  32131  rossros  32148  measvun  32177  ismbfm  32219  isanmbfm  32223  dya2iocuni  32250  oms0  32264  omssubadd  32267  carsgsigalem  32282  fiunelcarsg  32283  carsgclctunlem1  32284  carsgclctunlem2  32286  carsgclctunlem3  32287  carsgclctun  32288  pmeasmono  32291  pmeasadd  32292  kur14  33178  ispconn  33185  cvmscbv  33220  cvmsi  33227  cvmsval  33228  nnuni  33692  dfrdg2  33771  brbigcup  34200  dfbigcup2  34201  fobigcup  34202  brapply  34240  dfrdg4  34253  isfne  34528  fneval  34541  fnemeet1  34555  fnemeet2  34556  fnejoin1  34557  fnejoin2  34558  tailfval  34561  ordtoplem  34624  onsucsuccmpi  34632  limsucncmpi  34634  ordcmp  34636  bj-ismoore  35276  dissneqlem  35511  finxpreclem3  35564  pibp19  35585  pibp21  35586  pibt2  35588  heicant  35812  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  mbfresfi  35823  cover2  35872  cover2g  35873  istotbnd3  35929  sstotbnd  35933  heiborlem1  35969  heiborlem6  35974  heiborlem8  35976  dmqseqim  36768  sn-iotauni  40193  isnacs3  40532  nacsfix  40534  pwelg  41167  mnuprdlem1  41890  mnuprdlem2  41891  mnuunid  41895  mnurndlem1  41899  ismnushort  41919  csbfv12gALTVD  42519  stoweidlem35  43576  stoweidlem39  43580  stoweidlem50  43591  stoweidlem57  43598  issal  43855  salunicl  43857  saluncl  43858  prsal  43859  salgenval  43862  intsaluni  43868  salgenn0  43870  salgencl  43871  sssalgen  43874  salgenss  43875  salgenuni  43876  issalgend  43877  dfsalgen2  43880  issalnnd  43884  meadjuni  43995  ismeannd  44005  omeunile  44043  caragenunicl  44062  isomennd  44069  issmflem  44263  onsetreclem1  46410