Theorem unieq 4867

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 3988	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4866	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4866	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3947	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1541  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  unieqi  4868  unieqd  4869  uniintsn  4933  iununi  5045  treq  5203  eqsnuniex  5297  elvvuni  5691  unielrel  6221  unixp0  6230  unixpid  6231  limeq  6318  unizlim  6430  iotauni2  6453  opabiotafun  6902  uniexg  7673  onsucuni2  7764  onuninsuci  7770  orduninsuc  7773  undefval  8206  en1b  8947  nnunifi  9175  fissuni  9241  infeq5i  9526  infeq5  9527  rnttrcl  9612  ttrclselem2  9616  trcl  9618  rankuni  9756  rankxplim3  9774  iunfictbso  10005  cflim2  10154  cfss  10156  cfslb  10157  fin2i  10186  fin1a2lem10  10300  fin1a2lem11  10301  fin1a2lem12  10302  itunisuc  10310  ituniiun  10313  hsmex  10323  dominf  10336  zornn0g  10396  dominfac  10464  wununi  10597  wunex2  10629  wuncval2  10638  incexclem  15743  mrcfval  17514  mrisval  17536  acsdrsel  18449  isacs4lem  18450  isacs5lem  18451  acsdrscl  18452  isps  18474  isdir  18504  sylow2a  19531  uniopn  22812  istopon  22827  eltg3  22877  tgdom  22893  indistopon  22916  cldval  22938  ntrfval  22939  clsfval  22940  mretopd  23007  neifval  23014  lpfval  23053  isperf  23066  tgrest  23074  ist0  23235  ist1  23236  ishaus  23237  iscnrm  23238  iscmp  23303  cmpcov  23304  cmpcovf  23306  cncmp  23307  fincmp  23308  cmpsublem  23314  cmpsub  23315  tgcmp  23316  cmpcld  23317  uncmp  23318  hauscmplem  23321  cmpfi  23323  isconn  23328  is1stc  23356  2ndc1stc  23366  2ndcsep  23374  isref  23424  isptfin  23431  islocfin  23432  comppfsc  23447  kgenval  23450  1stckgenlem  23468  txcmplem1  23556  txcmplem2  23557  kqval  23641  flffval  23904  fclsval  23923  fcfval  23948  alexsublem  23959  alexsubb  23961  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  alexsubALT  23966  ptcmplem2  23968  ptcmplem3  23969  ptcmplem5  23971  cnextval  23976  iscfilu  24202  icccmplem1  24738  icccmplem2  24739  bndth  24884  lebnumlem3  24889  om1val  24957  pi1val  24964  ovolicc2  25450  isplig  30456  hsupval  31314  acunirnmpt  32641  iscref  33857  crefi  33860  cmpcref  33863  pcmplfin  33873  sigaclcu  34130  prsiga  34144  sigaclci  34145  unelsiga  34147  sigagenval  34153  unelldsys  34171  sigapildsys  34175  ldgenpisyslem1  34176  rossros  34193  measvun  34222  ismbfm  34264  dya2iocuni  34296  oms0  34310  omssubadd  34313  carsgsigalem  34328  fiunelcarsg  34329  carsgclctunlem1  34330  carsgclctunlem2  34332  carsgclctunlem3  34333  carsgclctun  34334  pmeasmono  34337  pmeasadd  34338  fissorduni  35101  fineqvnttrclselem2  35142  wevgblacfn  35153  kur14  35260  ispconn  35267  cvmscbv  35302  cvmsi  35309  cvmsval  35310  nnuni  35771  dfrdg2  35837  brbigcup  35940  dfbigcup2  35941  fobigcup  35942  brapply  35980  dfrdg4  35995  isfne  36383  fneval  36396  fnemeet1  36410  fnemeet2  36411  fnejoin1  36412  fnejoin2  36413  tailfval  36416  ordtoplem  36479  onsucsuccmpi  36487  limsucncmpi  36489  ordcmp  36491  bj-ismoore  37149  dissneqlem  37384  finxpreclem3  37437  pibp19  37458  pibp21  37459  pibt2  37461  heicant  37705  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  mbfresfi  37716  cover2  37765  cover2g  37766  istotbnd3  37821  sstotbnd  37825  heiborlem1  37861  heiborlem6  37866  heiborlem8  37868  dmqseqim  38764  isnacs3  42813  nacsfix  42815  onsupnmax  43331  onov0suclim  43377  pwelg  43663  mnuprdlem1  44375  mnuprdlem2  44376  mnuunid  44380  mnurndlem1  44384  ismnushort  44404  csbfv12gALTVD  45001  stoweidlem35  46143  stoweidlem39  46147  stoweidlem50  46158  stoweidlem57  46165  issal  46422  salunicl  46424  saluncl  46425  prsal  46426  salgenval  46429  intsaluni  46437  salgenn0  46439  salgencl  46440  sssalgen  46443  salgenss  46444  salgenuni  46445  issalgend  46446  dfsalgen2  46449  issalnnd  46453  meadjuni  46565  ismeannd  46575  omeunile  46613  caragenunicl  46632  isomennd  46639  issmflem  46835  termco  49592  onsetreclem1  49816