Theorem unieq 4861

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unieqi  4862  unieqd  4863  uniintsn  4927  iununi  5041  treq  5199  eqsnuniex  5303  elvvuni  5708  unielrel  6238  unixp0  6247  unixpid  6248  limeq  6335  unizlim  6447  iotauni2  6470  opabiotafun  6920  uniexg  7694  onsucuni2  7785  onuninsuci  7791  orduninsuc  7794  undefval  8226  en1b  8972  nnunifi  9201  fissuni  9267  infeq5i  9557  infeq5  9558  rnttrcl  9643  ttrclselem2  9647  trcl  9649  rankuni  9787  rankxplim3  9805  iunfictbso  10036  cflim2  10185  cfss  10187  cfslb  10188  fin2i  10217  fin1a2lem10  10331  fin1a2lem11  10332  fin1a2lem12  10333  itunisuc  10341  ituniiun  10344  hsmex  10354  dominf  10367  zornn0g  10427  dominfac  10496  wununi  10629  wunex2  10661  wuncval2  10670  incexclem  15801  mrcfval  17574  mrisval  17596  acsdrsel  18509  isacs4lem  18510  isacs5lem  18511  acsdrscl  18512  isps  18534  isdir  18564  sylow2a  19594  uniopn  22862  istopon  22877  eltg3  22927  tgdom  22943  indistopon  22966  cldval  22988  ntrfval  22989  clsfval  22990  mretopd  23057  neifval  23064  lpfval  23103  isperf  23116  tgrest  23124  ist0  23285  ist1  23286  ishaus  23287  iscnrm  23288  iscmp  23353  cmpcov  23354  cmpcovf  23356  cncmp  23357  fincmp  23358  cmpsublem  23364  cmpsub  23365  tgcmp  23366  cmpcld  23367  uncmp  23368  hauscmplem  23371  cmpfi  23373  isconn  23378  is1stc  23406  2ndc1stc  23416  2ndcsep  23424  isref  23474  isptfin  23481  islocfin  23482  comppfsc  23497  kgenval  23500  1stckgenlem  23518  txcmplem1  23606  txcmplem2  23607  kqval  23691  flffval  23954  fclsval  23973  fcfval  23998  alexsublem  24009  alexsubb  24011  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  ptcmplem2  24018  ptcmplem3  24019  ptcmplem5  24021  cnextval  24026  iscfilu  24252  icccmplem1  24788  icccmplem2  24789  bndth  24925  lebnumlem3  24930  om1val  24997  pi1val  25004  ovolicc2  25489  isplig  30547  hsupval  31405  acunirnmpt  32732  iscref  33988  crefi  33991  cmpcref  33994  pcmplfin  34004  sigaclcu  34261  prsiga  34275  sigaclci  34276  unelsiga  34278  sigagenval  34284  unelldsys  34302  sigapildsys  34306  ldgenpisyslem1  34307  rossros  34324  measvun  34353  ismbfm  34395  dya2iocuni  34427  oms0  34441  omssubadd  34444  carsgsigalem  34459  fiunelcarsg  34460  carsgclctunlem1  34461  carsgclctunlem2  34463  carsgclctunlem3  34464  carsgclctun  34465  pmeasmono  34468  pmeasadd  34469  fissorduni  35233  fineqvnttrclselem2  35266  wevgblacfn  35291  kur14  35398  ispconn  35405  cvmscbv  35440  cvmsi  35447  cvmsval  35448  nnuni  35909  dfrdg2  35975  brbigcup  36078  dfbigcup2  36079  fobigcup  36080  brapply  36118  dfrdg4  36133  isfne  36521  fneval  36534  fnemeet1  36548  fnemeet2  36549  fnejoin1  36550  fnejoin2  36551  tailfval  36554  ordtoplem  36617  onsucsuccmpi  36625  limsucncmpi  36627  ordcmp  36629  ttctr  36675  ttcmin  36678  dfttc2g  36688  bj-ismoore  37417  dissneqlem  37656  finxpreclem3  37709  pibp19  37730  pibp21  37731  pibt2  37733  heicant  37976  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  cover2  38036  cover2g  38037  istotbnd3  38092  sstotbnd  38096  heiborlem1  38132  heiborlem6  38137  heiborlem8  38139  dmqseqim  39062  isnacs3  43142  nacsfix  43144  onsupnmax  43656  onov0suclim  43702  pwelg  43987  mnuprdlem1  44699  mnuprdlem2  44700  mnuunid  44704  mnurndlem1  44708  ismnushort  44728  csbfv12gALTVD  45325  stoweidlem35  46463  stoweidlem39  46467  stoweidlem50  46478  stoweidlem57  46485  issal  46742  salunicl  46744  saluncl  46745  prsal  46746  salgenval  46749  intsaluni  46757  salgenn0  46759  salgencl  46760  sssalgen  46763  salgenss  46764  salgenuni  46765  issalgend  46766  dfsalgen2  46769  issalnnd  46773  meadjuni  46885  ismeannd  46895  omeunile  46933  caragenunicl  46952  isomennd  46959  issmflem  47155  termco  49956  onsetreclem1  50180