Theorem unieq 4862

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 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3982	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3940	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unieqi  4863  unieqd  4864  uniintsn  4928  iununi  5042  treq  5200  eqsnuniex  5296  elvvuni  5699  unielrel  6230  unixp0  6239  unixpid  6240  limeq  6327  unizlim  6439  iotauni2  6462  opabiotafun  6912  uniexg  7685  onsucuni2  7776  onuninsuci  7782  orduninsuc  7785  undefval  8217  en1b  8963  nnunifi  9192  fissuni  9258  infeq5i  9546  infeq5  9547  rnttrcl  9632  ttrclselem2  9636  trcl  9638  rankuni  9776  rankxplim3  9794  iunfictbso  10025  cflim2  10174  cfss  10176  cfslb  10177  fin2i  10206  fin1a2lem10  10320  fin1a2lem11  10321  fin1a2lem12  10322  itunisuc  10330  ituniiun  10333  hsmex  10343  dominf  10356  zornn0g  10416  dominfac  10485  wununi  10618  wunex2  10650  wuncval2  10659  incexclem  15790  mrcfval  17563  mrisval  17585  acsdrsel  18498  isacs4lem  18499  isacs5lem  18500  acsdrscl  18501  isps  18523  isdir  18553  sylow2a  19583  uniopn  22871  istopon  22886  eltg3  22936  tgdom  22952  indistopon  22975  cldval  22997  ntrfval  22998  clsfval  22999  mretopd  23066  neifval  23073  lpfval  23112  isperf  23125  tgrest  23133  ist0  23294  ist1  23295  ishaus  23296  iscnrm  23297  iscmp  23362  cmpcov  23363  cmpcovf  23365  cncmp  23366  fincmp  23367  cmpsublem  23373  cmpsub  23374  tgcmp  23375  cmpcld  23376  uncmp  23377  hauscmplem  23380  cmpfi  23382  isconn  23387  is1stc  23415  2ndc1stc  23425  2ndcsep  23433  isref  23483  isptfin  23490  islocfin  23491  comppfsc  23506  kgenval  23509  1stckgenlem  23527  txcmplem1  23615  txcmplem2  23616  kqval  23700  flffval  23963  fclsval  23982  fcfval  24007  alexsublem  24018  alexsubb  24020  alexsubALTlem2  24022  alexsubALTlem3  24023  alexsubALTlem4  24024  alexsubALT  24025  ptcmplem2  24027  ptcmplem3  24028  ptcmplem5  24030  cnextval  24035  iscfilu  24261  icccmplem1  24797  icccmplem2  24798  bndth  24934  lebnumlem3  24939  om1val  25006  pi1val  25013  ovolicc2  25498  isplig  30567  hsupval  31425  acunirnmpt  32752  iscref  34009  crefi  34012  cmpcref  34015  pcmplfin  34025  sigaclcu  34282  prsiga  34296  sigaclci  34297  unelsiga  34299  sigagenval  34305  unelldsys  34323  sigapildsys  34327  ldgenpisyslem1  34328  rossros  34345  measvun  34374  ismbfm  34416  dya2iocuni  34448  oms0  34462  omssubadd  34465  carsgsigalem  34480  fiunelcarsg  34481  carsgclctunlem1  34482  carsgclctunlem2  34484  carsgclctunlem3  34485  carsgclctun  34486  pmeasmono  34489  pmeasadd  34490  fissorduni  35254  fineqvnttrclselem2  35287  wevgblacfn  35312  kur14  35419  ispconn  35426  cvmscbv  35461  cvmsi  35468  cvmsval  35469  nnuni  35930  dfrdg2  35996  brbigcup  36099  dfbigcup2  36100  fobigcup  36101  brapply  36139  dfrdg4  36154  isfne  36542  fneval  36555  fnemeet1  36569  fnemeet2  36570  fnejoin1  36571  fnejoin2  36572  tailfval  36575  ordtoplem  36638  onsucsuccmpi  36646  limsucncmpi  36648  ordcmp  36650  ttctr  36696  ttcmin  36699  dfttc2g  36709  bj-ismoore  37430  dissneqlem  37667  finxpreclem3  37720  pibp19  37741  pibp21  37742  pibt2  37744  heicant  37987  ovoliunnfl  37994  voliunnfl  37996  volsupnfl  37997  mbfresfi  37998  cover2  38047  cover2g  38048  istotbnd3  38103  sstotbnd  38107  heiborlem1  38143  heiborlem6  38148  heiborlem8  38150  dmqseqim  39073  isnacs3  43153  nacsfix  43155  onsupnmax  43671  onov0suclim  43717  pwelg  44002  mnuprdlem1  44714  mnuprdlem2  44715  mnuunid  44719  mnurndlem1  44723  ismnushort  44743  csbfv12gALTVD  45340  stoweidlem35  46478  stoweidlem39  46482  stoweidlem50  46493  stoweidlem57  46500  issal  46757  salunicl  46759  saluncl  46760  prsal  46761  salgenval  46764  intsaluni  46772  salgenn0  46774  salgencl  46775  sssalgen  46778  salgenss  46779  salgenuni  46780  issalgend  46781  dfsalgen2  46784  issalnnd  46788  meadjuni  46900  ismeannd  46910  omeunile  46948  caragenunicl  46967  isomennd  46974  issmflem  47170  termco  49953  onsetreclem1  50177