Theorem unieq 4918

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 4042	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4917	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4043	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4917	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 4001	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unieqi  4919  unieqd  4920  uniintsn  4985  iununi  5099  treq  5267  eqsnuniex  5361  elvvuni  5762  unielrel  6294  unixp0  6303  unixpid  6304  limeq  6396  unizlim  6507  iotauni2  6530  opabiotafun  6989  uniexg  7760  onsucuni2  7854  onuninsuci  7861  orduninsuc  7864  undefval  8301  en1b  9065  nnunifi  9327  fissuni  9397  infeq5i  9676  infeq5  9677  rnttrcl  9762  ttrclselem2  9766  trcl  9768  rankuni  9903  rankxplim3  9921  iunfictbso  10154  cflim2  10303  cfss  10305  cfslb  10306  fin2i  10335  fin1a2lem10  10449  fin1a2lem11  10450  fin1a2lem12  10451  itunisuc  10459  ituniiun  10462  hsmex  10472  dominf  10485  zornn0g  10545  dominfac  10613  wununi  10746  wunex2  10778  wuncval2  10787  incexclem  15872  mrcfval  17651  mrisval  17673  acsdrsel  18588  isacs4lem  18589  isacs5lem  18590  acsdrscl  18591  isps  18613  isdir  18643  sylow2a  19637  uniopn  22903  istopon  22918  eltg3  22969  tgdom  22985  indistopon  23008  cldval  23031  ntrfval  23032  clsfval  23033  mretopd  23100  neifval  23107  lpfval  23146  isperf  23159  tgrest  23167  ist0  23328  ist1  23329  ishaus  23330  iscnrm  23331  iscmp  23396  cmpcov  23397  cmpcovf  23399  cncmp  23400  fincmp  23401  cmpsublem  23407  cmpsub  23408  tgcmp  23409  cmpcld  23410  uncmp  23411  hauscmplem  23414  cmpfi  23416  isconn  23421  is1stc  23449  2ndc1stc  23459  2ndcsep  23467  isref  23517  isptfin  23524  islocfin  23525  comppfsc  23540  kgenval  23543  1stckgenlem  23561  txcmplem1  23649  txcmplem2  23650  kqval  23734  flffval  23997  fclsval  24016  fcfval  24041  alexsublem  24052  alexsubb  24054  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem2  24061  ptcmplem3  24062  ptcmplem5  24064  cnextval  24069  iscfilu  24297  icccmplem1  24844  icccmplem2  24845  bndth  24990  lebnumlem3  24995  om1val  25063  pi1val  25070  ovolicc2  25557  isplig  30495  hsupval  31353  acunirnmpt  32669  iscref  33843  crefi  33846  cmpcref  33849  pcmplfin  33859  sigaclcu  34118  prsiga  34132  sigaclci  34133  unelsiga  34135  sigagenval  34141  unelldsys  34159  sigapildsys  34163  ldgenpisyslem1  34164  rossros  34181  measvun  34210  ismbfm  34252  dya2iocuni  34285  oms0  34299  omssubadd  34302  carsgsigalem  34317  fiunelcarsg  34318  carsgclctunlem1  34319  carsgclctunlem2  34321  carsgclctunlem3  34322  carsgclctun  34323  pmeasmono  34326  pmeasadd  34327  wevgblacfn  35114  kur14  35221  ispconn  35228  cvmscbv  35263  cvmsi  35270  cvmsval  35271  nnuni  35727  dfrdg2  35796  brbigcup  35899  dfbigcup2  35900  fobigcup  35901  brapply  35939  dfrdg4  35952  isfne  36340  fneval  36353  fnemeet1  36367  fnemeet2  36368  fnejoin1  36369  fnejoin2  36370  tailfval  36373  ordtoplem  36436  onsucsuccmpi  36444  limsucncmpi  36446  ordcmp  36448  bj-ismoore  37106  dissneqlem  37341  finxpreclem3  37394  pibp19  37415  pibp21  37416  pibt2  37418  heicant  37662  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  cover2  37722  cover2g  37723  istotbnd3  37778  sstotbnd  37782  heiborlem1  37818  heiborlem6  37823  heiborlem8  37825  dmqseqim  38657  isnacs3  42721  nacsfix  42723  onsupnmax  43240  onov0suclim  43287  pwelg  43573  mnuprdlem1  44291  mnuprdlem2  44292  mnuunid  44296  mnurndlem1  44300  ismnushort  44320  csbfv12gALTVD  44919  stoweidlem35  46050  stoweidlem39  46054  stoweidlem50  46065  stoweidlem57  46072  issal  46329  salunicl  46331  saluncl  46332  prsal  46333  salgenval  46336  intsaluni  46344  salgenn0  46346  salgencl  46347  sssalgen  46350  salgenss  46351  salgenuni  46352  issalgend  46353  dfsalgen2  46356  issalnnd  46360  meadjuni  46472  ismeannd  46482  omeunile  46520  caragenunicl  46539  isomennd  46546  issmflem  46742  onsetreclem1  49224