Theorem unieq 4847

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 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4846	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3974	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4846	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3934	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1539  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unieqi  4849  unieqd  4850  uniintsn  4915  iununi  5024  treq  5193  eqsnuniex  5278  elvvuni  5654  unielrel  6166  unixp0  6175  unixpid  6176  limeq  6263  unizlim  6368  opabiotafun  6831  uniexg  7571  onsucuni2  7656  onuninsuci  7662  orduninsuc  7665  undefval  8063  en1b  8767  en1bOLD  8768  nnunifi  8995  fissuni  9054  infeq5i  9324  infeq5  9325  trcl  9417  rankuni  9552  rankxplim3  9570  iunfictbso  9801  cflim2  9950  cfss  9952  cfslb  9953  fin2i  9982  fin1a2lem10  10096  fin1a2lem11  10097  fin1a2lem12  10098  itunisuc  10106  ituniiun  10109  hsmex  10119  dominf  10132  zornn0g  10192  dominfac  10260  wununi  10393  wunex2  10425  wuncval2  10434  incexclem  15476  mrcfval  17234  mrisval  17256  acsdrsel  18176  isacs4lem  18177  isacs5lem  18178  acsdrscl  18179  isps  18201  isdir  18231  sylow2a  19139  uniopn  21954  istopon  21969  eltg3  22020  tgdom  22036  indistopon  22059  cldval  22082  ntrfval  22083  clsfval  22084  mretopd  22151  neifval  22158  lpfval  22197  isperf  22210  tgrest  22218  ist0  22379  ist1  22380  ishaus  22381  iscnrm  22382  iscmp  22447  cmpcov  22448  cmpcovf  22450  cncmp  22451  fincmp  22452  cmpsublem  22458  cmpsub  22459  tgcmp  22460  cmpcld  22461  uncmp  22462  hauscmplem  22465  cmpfi  22467  isconn  22472  is1stc  22500  2ndc1stc  22510  2ndcsep  22518  isref  22568  isptfin  22575  islocfin  22576  comppfsc  22591  kgenval  22594  1stckgenlem  22612  txcmplem1  22700  txcmplem2  22701  kqval  22785  flffval  23048  fclsval  23067  fcfval  23092  alexsublem  23103  alexsubb  23105  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem2  23112  ptcmplem3  23113  ptcmplem5  23115  cnextval  23120  iscfilu  23348  icccmplem1  23891  icccmplem2  23892  bndth  24027  lebnumlem3  24032  om1val  24099  pi1val  24106  ovolicc2  24591  isplig  28739  hsupval  29597  acunirnmpt  30898  iscref  31696  crefi  31699  cmpcref  31702  pcmplfin  31712  sigaclcu  31985  prsiga  31999  sigaclci  32000  unelsiga  32002  sigagenval  32008  unelldsys  32026  sigapildsys  32030  ldgenpisyslem1  32031  rossros  32048  measvun  32077  ismbfm  32119  isanmbfm  32123  dya2iocuni  32150  oms0  32164  omssubadd  32167  carsgsigalem  32182  fiunelcarsg  32183  carsgclctunlem1  32184  carsgclctunlem2  32186  carsgclctunlem3  32187  carsgclctun  32188  pmeasmono  32191  pmeasadd  32192  kur14  33078  ispconn  33085  cvmscbv  33120  cvmsi  33127  cvmsval  33128  nnuni  33595  dfrdg2  33677  rnttrcl  33708  ttrclselem2  33712  brbigcup  34127  dfbigcup2  34128  fobigcup  34129  brapply  34167  dfrdg4  34180  isfne  34455  fneval  34468  fnemeet1  34482  fnemeet2  34483  fnejoin1  34484  fnejoin2  34485  tailfval  34488  ordtoplem  34551  onsucsuccmpi  34559  limsucncmpi  34561  ordcmp  34563  bj-ismoore  35203  dissneqlem  35438  finxpreclem3  35491  pibp19  35512  pibp21  35513  pibt2  35515  heicant  35739  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  cover2  35799  cover2g  35800  istotbnd3  35856  sstotbnd  35860  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  dmqseqim  36695  sn-iotauni  40120  isnacs3  40448  nacsfix  40450  pwelg  41056  mnuprdlem1  41779  mnuprdlem2  41780  mnuunid  41784  mnurndlem1  41788  ismnushort  41808  csbfv12gALTVD  42408  stoweidlem35  43466  stoweidlem39  43470  stoweidlem50  43481  stoweidlem57  43488  issal  43745  salunicl  43747  saluncl  43748  prsal  43749  salgenval  43752  intsaluni  43758  salgenn0  43760  salgencl  43761  sssalgen  43764  salgenss  43765  salgenuni  43766  issalgend  43767  dfsalgen2  43770  issalnnd  43774  meadjuni  43885  ismeannd  43895  omeunile  43933  caragenunicl  43952  isomennd  43959  issmflem  44150  onsetreclem1  46296