Theorem unieq 4885

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 4008	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4884	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4009	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4884	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3967	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unieqi  4886  unieqd  4887  uniintsn  4952  iununi  5066  treq  5225  eqsnuniex  5319  elvvuni  5718  unielrel  6250  unixp0  6259  unixpid  6260  limeq  6347  unizlim  6460  iotauni2  6483  opabiotafun  6944  uniexg  7719  onsucuni2  7812  onuninsuci  7819  orduninsuc  7822  undefval  8258  en1b  8999  nnunifi  9245  fissuni  9315  infeq5i  9596  infeq5  9597  rnttrcl  9682  ttrclselem2  9686  trcl  9688  rankuni  9823  rankxplim3  9841  iunfictbso  10074  cflim2  10223  cfss  10225  cfslb  10226  fin2i  10255  fin1a2lem10  10369  fin1a2lem11  10370  fin1a2lem12  10371  itunisuc  10379  ituniiun  10382  hsmex  10392  dominf  10405  zornn0g  10465  dominfac  10533  wununi  10666  wunex2  10698  wuncval2  10707  incexclem  15809  mrcfval  17576  mrisval  17598  acsdrsel  18509  isacs4lem  18510  isacs5lem  18511  acsdrscl  18512  isps  18534  isdir  18564  sylow2a  19556  uniopn  22791  istopon  22806  eltg3  22856  tgdom  22872  indistopon  22895  cldval  22917  ntrfval  22918  clsfval  22919  mretopd  22986  neifval  22993  lpfval  23032  isperf  23045  tgrest  23053  ist0  23214  ist1  23215  ishaus  23216  iscnrm  23217  iscmp  23282  cmpcov  23283  cmpcovf  23285  cncmp  23286  fincmp  23287  cmpsublem  23293  cmpsub  23294  tgcmp  23295  cmpcld  23296  uncmp  23297  hauscmplem  23300  cmpfi  23302  isconn  23307  is1stc  23335  2ndc1stc  23345  2ndcsep  23353  isref  23403  isptfin  23410  islocfin  23411  comppfsc  23426  kgenval  23429  1stckgenlem  23447  txcmplem1  23535  txcmplem2  23536  kqval  23620  flffval  23883  fclsval  23902  fcfval  23927  alexsublem  23938  alexsubb  23940  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  ptcmplem2  23947  ptcmplem3  23948  ptcmplem5  23950  cnextval  23955  iscfilu  24182  icccmplem1  24718  icccmplem2  24719  bndth  24864  lebnumlem3  24869  om1val  24937  pi1val  24944  ovolicc2  25430  isplig  30412  hsupval  31270  acunirnmpt  32590  iscref  33841  crefi  33844  cmpcref  33847  pcmplfin  33857  sigaclcu  34114  prsiga  34128  sigaclci  34129  unelsiga  34131  sigagenval  34137  unelldsys  34155  sigapildsys  34159  ldgenpisyslem1  34160  rossros  34177  measvun  34206  ismbfm  34248  dya2iocuni  34281  oms0  34295  omssubadd  34298  carsgsigalem  34313  fiunelcarsg  34314  carsgclctunlem1  34315  carsgclctunlem2  34317  carsgclctunlem3  34318  carsgclctun  34319  pmeasmono  34322  pmeasadd  34323  wevgblacfn  35103  kur14  35210  ispconn  35217  cvmscbv  35252  cvmsi  35259  cvmsval  35260  nnuni  35721  dfrdg2  35790  brbigcup  35893  dfbigcup2  35894  fobigcup  35895  brapply  35933  dfrdg4  35946  isfne  36334  fneval  36347  fnemeet1  36361  fnemeet2  36362  fnejoin1  36363  fnejoin2  36364  tailfval  36367  ordtoplem  36430  onsucsuccmpi  36438  limsucncmpi  36440  ordcmp  36442  bj-ismoore  37100  dissneqlem  37335  finxpreclem3  37388  pibp19  37409  pibp21  37410  pibt2  37412  heicant  37656  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfresfi  37667  cover2  37716  cover2g  37717  istotbnd3  37772  sstotbnd  37776  heiborlem1  37812  heiborlem6  37817  heiborlem8  37819  dmqseqim  38655  isnacs3  42705  nacsfix  42707  onsupnmax  43224  onov0suclim  43270  pwelg  43556  mnuprdlem1  44268  mnuprdlem2  44269  mnuunid  44273  mnurndlem1  44277  ismnushort  44297  csbfv12gALTVD  44895  stoweidlem35  46040  stoweidlem39  46044  stoweidlem50  46055  stoweidlem57  46062  issal  46319  salunicl  46321  saluncl  46322  prsal  46323  salgenval  46326  intsaluni  46334  salgenn0  46336  salgencl  46337  sssalgen  46340  salgenss  46341  salgenuni  46342  issalgend  46343  dfsalgen2  46346  issalnnd  46350  meadjuni  46462  ismeannd  46472  omeunile  46510  caragenunicl  46529  isomennd  46536  issmflem  46732  termco  49474  onsetreclem1  49698