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 1560  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4866

This theorem is referenced by:  unieqi  4877  unieqd  4878  uniintsn  4943  iununi  5056  treq  5214  eqsnuniex  5318  elvvuni  5724  unielrel  6261  unixp0  6270  unixpid  6271  limeq  6358  unizlim  6470  iotauni2  6493  opabiotafun  6947  uniexg  7723  onsucuni2  7814  onuninsuci  7820  orduninsuc  7823  undefval  8257  en1b  9006  nnunifi  9235  fissuni  9300  infeq5i  9591  infeq5  9592  rnttrcl  9677  ttrclselem2  9681  trcl  9683  rankuni  9821  rankxplim3  9839  iunfictbso  10070  cflim2  10220  cfss  10222  cfslb  10223  fin2i  10252  fin1a2lem10  10366  fin1a2lem11  10367  fin1a2lem12  10368  itunisuc  10376  ituniiun  10379  hsmex  10389  dominf  10402  zornn0g  10462  dominfac  10531  wununi  10664  wunex2  10696  wuncval2  10705  incexclem  15866  mrcfval  17640  mrisval  17662  acsdrsel  18575  isacs4lem  18576  isacs5lem  18577  acsdrscl  18578  isps  18600  isdir  18630  sylow2a  19659  uniopn  22957  istopon  22972  eltg3  23022  tgdom  23038  indistopon  23061  cldval  23083  ntrfval  23084  clsfval  23085  mretopd  23152  neifval  23159  lpfval  23198  isperf  23211  tgrest  23219  ist0  23380  ist1  23381  ishaus  23382  iscnrm  23383  iscmp  23448  cmpcov  23449  cmpcovf  23451  cncmp  23452  fincmp  23453  cmpsublem  23459  cmpsub  23460  tgcmp  23461  cmpcld  23462  uncmp  23463  hauscmplem  23466  cmpfi  23468  isconn  23473  is1stc  23501  2ndc1stc  23511  2ndcsep  23519  isref  23569  isptfin  23576  islocfin  23577  comppfsc  23592  kgenval  23595  1stckgenlem  23613  txcmplem1  23701  txcmplem2  23702  kqval  23786  flffval  24049  fclsval  24068  fcfval  24093  alexsublem  24104  alexsubb  24106  alexsubALTlem2  24108  alexsubALTlem3  24109  alexsubALTlem4  24110  alexsubALT  24111  ptcmplem2  24113  ptcmplem3  24114  ptcmplem5  24116  cnextval  24121  iscfilu  24347  icccmplem1  24883  icccmplem2  24884  bndth  25020  lebnumlem3  25025  om1val  25092  pi1val  25099  ovolicc2  25584  isplig  30679  hsupval  31537  acunirnmpt  32861  iscref  34141  crefi  34144  cmpcref  34147  pcmplfin  34157  sigaclcu  34414  prsiga  34428  sigaclci  34429  unelsiga  34431  sigagenval  34437  unelldsys  34455  sigapildsys  34459  ldgenpisyslem1  34460  rossros  34477  measvun  34506  ismbfm  34548  dya2iocuni  34580  oms0  34594  omssubadd  34597  carsgsigalem  34612  fiunelcarsg  34613  carsgclctunlem1  34614  carsgclctunlem2  34616  carsgclctunlem3  34617  carsgclctun  34618  pmeasmono  34621  pmeasadd  34622  fissorduni  35385  fineqvnttrclselem2  35418  wevgblacfn  35454  kur14  35566  ispconn  35573  cvmscbv  35608  cvmsi  35615  cvmsval  35616  nnuni  36077  dfrdg2  36143  brbigcup  36246  dfbigcup2  36247  fobigcup  36248  brapply  36286  dfrdg4  36301  isfne  36699  fneval  36712  fnemeet1  36726  fnemeet2  36727  fnejoin1  36728  fnejoin2  36729  tailfval  36732  ordtoplem  36795  onsucsuccmpi  36803  limsucncmpi  36805  ordcmp  36807  ttctr  36853  ttcmin  36856  dfttc2g  36866  bj-ismoore  37595  dissneqlem  37834  finxpreclem3  37887  pibp19  37908  pibp21  37909  pibt2  37911  heicant  38154  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  mbfresfi  38165  cover2  38214  cover2g  38215  istotbnd3  38270  sstotbnd  38274  heiborlem1  38310  heiborlem6  38315  heiborlem8  38317  dmqseqim  39240  isnacs3  43291  nacsfix  43293  onsupnmax  43805  onov0suclim  43851  pwelg  44136  mnuprdlem1  44848  mnuprdlem2  44849  mnuunid  44853  mnurndlem1  44857  ismnushort  44877  csbfv12gALTVD  45474  stoweidlem35  46609  stoweidlem39  46613  stoweidlem50  46624  stoweidlem57  46631  issal  46888  salunicl  46890  saluncl  46891  prsal  46892  salgenval  46895  intsaluni  46903  salgenn0  46905  salgencl  46906  sssalgen  46909  salgenss  46910  salgenuni  46911  issalgend  46912  dfsalgen2  46915  issalnnd  46919  meadjuni  47031  ismeannd  47041  omeunile  47079  caragenunicl  47098  isomennd  47105  issmflem  47301  termco  50102  onsetreclem1  50326